Commit 2026-08-12 12:06 f4bdd07c

View on Github →

chore(Algebra): remove references to NoZeroSMulDivisors (#42166) Follow-up to #30563 and #33873. Removes references to NoZeroSMulDivisors in places where it no longer appears, and renames some lemmas which now use IsTorsionFree instead of NoZeroSMulDivisors.

Estimated changes

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

added theorem Ideal.torsionOf_eq_bot_iff_of_isTorsionFree

deleted theorem Ideal.torsionOf_eq_bot_iff_of_noZeroSMulDivisors

Modified Mathlib/Algebra/Polynomial/Roots.lean

Modified Mathlib/RingTheory/AdjoinRoot.lean

added theorem AdjoinRoot.isTorsionFree_of_prime_of_degree_ne_zero

deleted theorem AdjoinRoot.noZeroSMulDivisors_of_prime_of_degree_ne_zero

Modified Mathlib/RingTheory/IsAdjoinRoot.lean

Modified Mathlib/RingTheory/Support.lean

added theorem Module.support_of_isTorsionFree

deleted theorem Module.support_of_noZeroSMulDivisors