Commit 2025-01-20 17:23 535a874a

View on Github →

feat(GroupTheory/SpecificGroups): dihedral groups are not cyclic (with one exception) (#20817)

Estimated changes

Modified Mathlib/Data/ZMod/Basic.lean

added theorem ZMod.val_two_eq_two_mod

Modified Mathlib/GroupTheory/SpecificGroups/Cyclic.lean

added theorem DihedralGroup.isCyclic_iff

added theorem DihedralGroup.not_isCyclic

Modified Mathlib/GroupTheory/SpecificGroups/Dihedral.lean

added theorem DihedralGroup.commutative_iff

added theorem DihedralGroup.not_commutative

Modified Mathlib/GroupTheory/SpecificGroups/KleinFour.lean

modified theorem IsKleinFour.not_isCyclic

Modified Mathlib/GroupTheory/Transfer.lean