Theorem Ideal.iInf_pow_smul_eq_bot_of_noZeroSMulDivisors

Modification history

2026-01-13 19:40
Mathlib/RingTheory/Filtration.lean
chore(Algebra): replace `NoZeroSMulDivisors` with `Module.IsTorsionFree` wlog (#30563) …
Deleted Ideal.iInf_pow_smul_eq_bot_of_noZeroSMulDivisorsView on Github →
2025-02-10 20:18
Mathlib/RingTheory/Filtration.lean
feat(RingTheory): Hausdorff-ness of Noetherian rings (#20425)
Added Ideal.iInf_pow_smul_eq_bot_of_noZeroSMulDivisorsView on Github →