Commit 2025-12-13 13:14 12884d8f

View on Github →

chore(Algebra): move CharZero.of_module earlier (#32834) This has nothing to do with NoZeroSMulDivisors.

Estimated changes

Modified Mathlib/Algebra/Module/NatInt.lean

added theorem CharZero.of_module

Modified Mathlib/Algebra/NoZeroSMulDivisors/Basic.lean

deleted theorem CharZero.of_module

Modified Mathlib/NumberTheory/NumberField/Basic.lean