Theorem flat_algebraMap_iff

Modification history

2025-08-15 15:34
Mathlib/RingTheory/RingHom/Flat.lean
feat(RingTheory): faithfully flat ring maps (#24530) …
Deleted flat_algebraMap_iffView on Github →
2025-04-03 11:07
Mathlib/RingTheory/RingHom/Flat.lean
feat(AlgebraicGeometry): faithfully flat morphisms are topological quotient maps (#23608)
Added flat_algebraMap_iffView on Github →