Theorem Module.Flat.flat_iff_torsion_eq_bot_of_valuationRing_localization_isMaximal

Modification history

2025-09-15 21:27
Mathlib/RingTheory/Flat/TorsionFree.lean
feat(RingTheory/Flat): Add theorems relating Submodule.torsion and Module.Flat (#26783)
Added Module.Flat.flat_iff_torsion_eq_bot_of_valuationRing_localization_isMaximalView on Github →