Theorem Module.IsTorsionFree.trans_faithfulSMul

Modification history

2026-01-26 15:41

Mathlib/Algebra/Algebra/Basic.lean

chore(Algebra): deprecate a few more `NoZeroSMulDivisors` lemmas (#34203) …

Modified Module.IsTorsionFree.trans_faithfulSMul View on Github →

2026-01-12 13:34

Mathlib/Algebra/Algebra/Basic.lean

feat(Algebra): more `Module.IsTorsionFree` API (#33871) …

Added Module.IsTorsionFree.trans_faithfulSMul View on Github →