Theorem RingHom.Flat.generalizingMap_comap

Modification history

2025-04-03 11:07
Mathlib/RingTheory/RingHom/Flat.lean
feat(AlgebraicGeometry): faithfully flat morphisms are topological quotient maps (#23608)
Added RingHom.Flat.generalizingMap_comapView on Github →