Commit 2024-11-06 11:22 3acb1eb2

View on Github →

feat: localization is flat (#18683)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Module/LocalizedModule/Submodule.lean

Created Mathlib/RingTheory/Flat/Localization.lean

added theorem IsLocalization.flat