Theorem Submodule.AddMonoid.IsTorsionFree_iff_noZeroSMulDivisors

Modification history

2024-02-29 21:30
Mathlib/Algebra/Module/Torsion.lean
feat: `IsTorsionFree M ↔ NoZeroSMulDivisors ℕ M` (#10918) …
Deleted Submodule.AddMonoid.IsTorsionFree_iff_noZeroSMulDivisorsView on Github →
2024-01-06 09:51
Mathlib/Algebra/Module/Torsion.lean
feat: Provide glue between `AddCommGroup` and `Module ℤ` (#9345)
Added Submodule.AddMonoid.IsTorsionFree_iff_noZeroSMulDivisorsView on Github →