Theorem NoZeroSMulDivisors.isReduced

Modification history

2026-05-17 20:27
Mathlib/RingTheory/Nilpotent/Basic.lean
chore: remove declarations deprecated between 2021-05-15 and 2025-11-15 (#39405) …
Deleted NoZeroSMulDivisors.isReducedView on Github →
2026-01-20 08:34
Mathlib/RingTheory/Nilpotent/Basic.lean
chore(Algebra): replace `NoZeroSMulDivisors` with `Module.IsTorsionFree`, losing generality (#33873) …
Modified NoZeroSMulDivisors.isReducedView on Github →
2024-04-23 14:29
Mathlib/RingTheory/Nilpotent.lean
chore: split RingTheory.Nilpotent (#12184) …
Modified NoZeroSMulDivisors.isReducedView on Github →
2023-11-03 16:55
Mathlib/RingTheory/Nilpotent.lean
feat: basic lemmas about nilpotency in rings (#8156)
Added NoZeroSMulDivisors.isReducedView on Github →