Commit 2025-01-21 06:28 6882ea71

View on Github →

refactor(Data/ZMod/Quotient): Split file (#20894) This PR splits Mathlib/Data/ZMod/Quotient.lean into a group-theory file and a ring-theory file. This makes sure that the file on cyclic groups doesn't import ideals.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Module/Torsion.lean

Renamed Mathlib/Data/ZMod/Quotient.lean to Mathlib/Data/ZMod/QuotientGroup.lean

deleted def Int.quotientSpanEquivZMod

deleted def Int.quotientSpanNatEquivZMod

deleted def ZMod.prodEquivPi

Created Mathlib/Data/ZMod/QuotientRing.lean

added def Int.quotientSpanEquivZMod

added def Int.quotientSpanNatEquivZMod

added def ZMod.prodEquivPi

Modified Mathlib/GroupTheory/FiniteAbelian/Basic.lean

Modified Mathlib/GroupTheory/SpecificGroups/Cyclic.lean

Modified Mathlib/LinearAlgebra/FreeModule/IdealQuotient.lean

Modified Mathlib/LinearAlgebra/FreeModule/Int.lean

Modified Mathlib/LinearAlgebra/Matrix/SpecialLinearGroup.lean

Modified Mathlib/MeasureTheory/Group/AddCircle.lean

Modified Mathlib/NumberTheory/Cyclotomic/CyclotomicCharacter.lean

Modified Mathlib/RingTheory/AdicCompletion/Algebra.lean

Modified Mathlib/RingTheory/DedekindDomain/SelmerGroup.lean