Theorem NoZeroSMulDivisors.smul_right_injective

Modification history

2026-01-20 08:34
Mathlib/Algebra/NoZeroSMulDivisors/Basic.lean
chore(Algebra): replace `NoZeroSMulDivisors` with `Module.IsTorsionFree`, losing generality (#33873) …
Deleted NoZeroSMulDivisors.smul_right_injectiveView on Github →
2026-01-13 19:40
Mathlib/Algebra/NoZeroSMulDivisors/Basic.lean
chore(Algebra): replace `NoZeroSMulDivisors` with `Module.IsTorsionFree` wlog (#30563) …
Added NoZeroSMulDivisors.smul_right_injectiveView on Github →