Theorem Module.isTorsionFree_iff_algebraMap_injective

Modification history

2026-01-26 15:41
Mathlib/Algebra/Algebra/Basic.lean
chore(Algebra): deprecate a few more `NoZeroSMulDivisors` lemmas (#34203) …
Modified Module.isTorsionFree_iff_algebraMap_injectiveView on Github →
2026-01-12 13:34
Mathlib/Algebra/Algebra/Basic.lean
feat(Algebra): more `Module.IsTorsionFree` API (#33871) …
Added Module.isTorsionFree_iff_algebraMap_injectiveView on Github →