Theorem Ideal.torsionOf_eq_bot_iff_of_isTorsionFree

Modification history

2026-08-12 12:06
Mathlib/Algebra/Module/Torsion/Basic.lean
chore(Algebra): remove references to `NoZeroSMulDivisors` (#42166) …
Added Ideal.torsionOf_eq_bot_iff_of_isTorsionFreeView on Github →