Theorem Module.flat_of_isLocalized_maixmal

Modification history

2024-12-20 22:32
Mathlib/RingTheory/Flat/Localization.lean
feat(RingTheory/Flat): generalize `flat_of_isLocalized_span` (#19788) …
Deleted Module.flat_of_isLocalized_maixmalView on Github →
2024-12-07 06:05
Mathlib/RingTheory/Flat/Localization.lean
feat(RingTheory/LocalProperties): flatness is a local property (#19085) …
Added Module.flat_of_isLocalized_maixmalView on Github →