Commit 2025-02-17 16:56 ae9822b4

View on Github →

refactor(GroupTheory/SpecificGroups/Cyclic,Dihedral): Reverse import (#20923) This PR makes Dihedral.lean import Cyclic.lean instead of the other way around.

Estimated changes

Modified Archive/Wiedijk100Theorems/AbelRuffini.lean

Modified Mathlib/Algebra/Group/Subgroup/ZPowers/Basic.lean

added theorem Int.zmultiples_natAbs

Modified Mathlib/Algebra/Module/Torsion.lean

Modified Mathlib/Algebra/Module/ZMod.lean

Modified Mathlib/Data/ZMod/QuotientGroup.lean

Modified Mathlib/FieldTheory/Finite/Basic.lean

Modified Mathlib/GroupTheory/Schreier.lean

Modified Mathlib/GroupTheory/SpecificGroups/Cyclic.lean

deleted theorem DihedralGroup.isCyclic_iff

deleted theorem DihedralGroup.not_isCyclic

Modified Mathlib/GroupTheory/SpecificGroups/Dihedral.lean

modified theorem DihedralGroup.commutative_iff

added theorem DihedralGroup.isCyclic_iff

added theorem DihedralGroup.not_isCyclic

Modified Mathlib/GroupTheory/SpecificGroups/Quaternion.lean

Modified Mathlib/GroupTheory/Torsion.lean

Modified Mathlib/LinearAlgebra/FreeModule/Int.lean

Modified Mathlib/RingTheory/Int/Basic.lean

deleted theorem Int.zmultiples_natAbs