Theorem NoZeroSMulDivisors.IsAddTorsionFree.of_noZeroSMulDivisors

Modification history

2026-01-20 08:34

Mathlib/Algebra/NoZeroSMulDivisors/Basic.lean

chore(Algebra): replace `NoZeroSMulDivisors` with `Module.IsTorsionFree`, losing generality (#33873) …

Deleted NoZeroSMulDivisors.IsAddTorsionFree.of_noZeroSMulDivisors View on Github →

2026-01-13 19:40

Mathlib/Algebra/NoZeroSMulDivisors/Basic.lean

chore(Algebra): replace `NoZeroSMulDivisors` with `Module.IsTorsionFree` wlog (#30563) …

Added NoZeroSMulDivisors.IsAddTorsionFree.of_noZeroSMulDivisors View on Github →