Revision #1458 → #3769 · back to history
modifiedParity of zero4f7407d4542a
| Field | From #1458 | To #3769 |
|---|
| note | Even.zero : Even (0 : α) is registered as a grind_pattern. | Even.zero : Even (0 : α) is registered in Mathlib.Algebra.Group.Even. |
modifiedParity as ring homomorphism7db832e1f06f
| Field | From #1458 | To #3769 |
|---|
| mathlib.module | Mathlib.Data.ZMod.Basic | Mathlib.Data.Int.Cast.Lemmas |
modifiedField with two elements structure3dc3551023fd
| Field | From #1458 | To #3769 |
|---|
| mathlib.module | Mathlib.Data.ZMod.Basic | Mathlib.Data.ZMod.Defs |
addedEven plus even is even87574a65e798
addedOdd number characterization (2k+1 form)a5d131b8d65d
addedInteger is even iff congruent to 0 mod 2259d95547b6f
addedRubik's cube uses only even permutations51bc1e9b18e1