Commit 2025-11-05 11:15 dbdc6d8a

View on Github →

chore: use IsAddTorsionFree M instead of NoZeroSMulDivisors ℕ M/NoZeroSMulDivisors ℤ M (#30683) These are all equivalent spellings, but the former works without knowing about Module.

Estimated changes

Modified Mathlib/Algebra/Lie/Sl2.lean

modified theorem IsSl2Triple.HasPrimitiveVectorWith.mk'

Modified Mathlib/Algebra/Lie/Weights/Chain.lean

Modified Mathlib/Algebra/Lie/Weights/Killing.lean

Modified Mathlib/Algebra/Module/Rat.lean

added theorem IsAddTorsionFree.of_module_nnrat

added theorem IsAddTorsionFree.of_module_rat

Modified Mathlib/Algebra/Module/Torsion.lean

modified theorem infinite_range_add_nsmul_iff

Modified Mathlib/Algebra/Module/ZLattice/Basic.lean

Modified Mathlib/Algebra/NoZeroSMulDivisors/Basic.lean

modified theorem CharZero.of_noZeroSMulDivisors

added theorem IsAddTorsionFree.of_noZeroSMulDivisors

Modified Mathlib/Algebra/Polynomial/Derivative.lean

modified theorem Polynomial.degree_derivative_eq

modified theorem Polynomial.eq_C_of_derivative_eq_zero

modified theorem Polynomial.mem_support_derivative

modified theorem Polynomial.natDegree_eq_zero_of_derivative_eq_zero

Modified Mathlib/Algebra/Polynomial/HasseDeriv.lean

modified theorem Polynomial.natDegree_hasseDeriv

Modified Mathlib/Algebra/Ring/CharZero.lean

Modified Mathlib/Analysis/Normed/Module/Ball/Action.lean

Modified Mathlib/Analysis/Normed/Module/Basic.lean

Modified Mathlib/GroupTheory/Subgroup/Saturated.lean

modified theorem AddSubgroup.ker_saturated

Modified Mathlib/LinearAlgebra/Basis/Submodule.lean

Modified Mathlib/LinearAlgebra/Reflection.lean

modified theorem Module.eq_of_mapsTo_reflection_of_mem

modified theorem Module.infinite_range_reflection_reflection_iterate_iff

modified theorem Module.injOn_dualMap_subtype_span_range_range

Modified Mathlib/LinearAlgebra/RootSystem/Base.lean

Modified Mathlib/LinearAlgebra/RootSystem/Basic.lean

modified theorem RootPairing.injOn_dualMap_subtype_span_root_coroot

Modified Mathlib/LinearAlgebra/RootSystem/Chain.lean

Modified Mathlib/LinearAlgebra/RootSystem/Defs.lean

modified theorem RootPairing.coroot_eq_smul_coroot_iff

modified theorem RootPairing.smul_coroot_eq_of_root_eq_smul

Modified Mathlib/LinearAlgebra/RootSystem/Finite/Lemmas.lean

Modified Mathlib/LinearAlgebra/RootSystem/GeckConstruction/Lemmas.lean

Modified Mathlib/LinearAlgebra/RootSystem/GeckConstruction/Relations.lean

Modified Mathlib/LinearAlgebra/RootSystem/GeckConstruction/Semisimple.lean

Modified Mathlib/LinearAlgebra/RootSystem/Reduced.lean

modified theorem RootPairing.coxeterWeight_ne_four_of_linearIndependent

modified theorem RootPairing.infinite_of_linearIndependent_coxeterWeight_four

modified theorem RootPairing.nsmul_notMem_range_root

Modified Mathlib/MeasureTheory/Group/Integral.lean

Modified Mathlib/RingTheory/Binomial.lean

Modified Mathlib/RingTheory/MvPolynomial/WeightedHomogeneous.lean

modified theorem MvPolynomial.nonTorsionWeight_of

modified theorem MvPolynomial.weightedHomogeneousComponent_zero

Modified Mathlib/RingTheory/PowerSeries/Derivative.lean

modified theorem PowerSeries.derivative.ext

Modified Mathlib/RingTheory/TensorProduct/Maps.lean

Modified Mathlib/Topology/Category/Profinite/Nobeling/ZeroLimit.lean