Theorem DihedralGroup.not_commutative

Modification history

2026-04-09 03:01
Mathlib/GroupTheory/SpecificGroups/Dihedral.lean
chore(Algebra): use `IsMulCommutative` to spell `Std.Commutative (· * ·)` (#37448) …
Modified DihedralGroup.not_commutativeView on Github →
2025-01-20 17:23
Mathlib/GroupTheory/SpecificGroups/Dihedral.lean
feat(GroupTheory/SpecificGroups): dihedral groups are not cyclic (with one exception) (#20817)
Added DihedralGroup.not_commutativeView on Github →