Commit 2024-09-30 09:29 e336e27e

View on Github →

chore(ZMod): Move module and algebra instances under Algebra (#17237) Those files have nothing to do under Data

Estimated changes

Modified Mathlib.lean

Renamed Mathlib/Data/ZMod/Algebra.lean to Mathlib/Algebra/Algebra/ZMod.lean

Modified Mathlib/Algebra/Module/Torsion.lean

Renamed Mathlib/Data/ZMod/Module.lean to Mathlib/Algebra/Module/ZMod.lean

Modified Mathlib/FieldTheory/Finite/GaloisField.lean

Modified Mathlib/FieldTheory/IsAlgClosed/Classification.lean

Modified Mathlib/RingTheory/Polynomial/Cyclotomic/Expand.lean

Modified Mathlib/RingTheory/WittVector/Frobenius.lean