Commit 2026-01-26 15:41 45edaee1

View on Github →

chore(Algebra): deprecate a few more NoZeroSMulDivisors lemmas (#34203) These were forgotten in #33873.

Estimated changes

Modified Mathlib/Algebra/Algebra/Basic.lean

modified theorem Module.IsTorsionFree.trans_faithfulSMul

modified theorem Module.isTorsionFree_iff_algebraMap_injective

modified theorem Module.isTorsionFree_iff_faithfulSMul

deleted theorem NoZeroSMulDivisors.iff_algebraMap_injective

deleted theorem NoZeroSMulDivisors.iff_faithfulSMul

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

modified theorem Module.isTorsionFree_iff_smul_eq_zero

Modified Mathlib/RingTheory/Extension/Generators.lean