Theorem Algebra.lsmul_injective

Modification history

2026-01-20 08:34

Mathlib/Algebra/Algebra/Tower.lean

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

Modified Algebra.lsmul_injective View on Github →

2023-03-01 10:14

Mathlib/Algebra/Algebra/Tower.lean

feat: Port Algebra.Algebra.Tower (#2548)

Added Algebra.lsmul_injective View on Github →