Theorem NoZeroSMulDivisors_of_isLocalization

Modification history

2026-01-13 19:40
Mathlib/RingTheory/Localization/Ideal.lean
chore(Algebra): replace `NoZeroSMulDivisors` with `Module.IsTorsionFree` wlog (#30563) …
Deleted NoZeroSMulDivisors_of_isLocalizationView on Github →
2025-02-03 10:21
Mathlib/RingTheory/Localization/Ideal.lean
feat: generalize `Ideal.spanNorm` to allow non free extensions (#19244) …
Added NoZeroSMulDivisors_of_isLocalizationView on Github →