Theorem Module.Flat.of_projective_surjective

Modification history

2025-01-17 07:37
Mathlib/RingTheory/Flat/Basic.lean
feat(RingTheory): flatness over a semiring (#19115) …
Deleted Module.Flat.of_projective_surjectiveView on Github →
2023-10-31 10:54
Mathlib/RingTheory/Flat.lean
feat(RingTheory/Flat): free and projective modules over a `CommRing` are flat (#7567) …
Added Module.Flat.of_projective_surjectiveView on Github →