Theorem RingHom.Flat.ofLocalizationPrime

Modification history

2025-01-18 20:53
Mathlib/RingTheory/RingHom/Flat.lean
feat(AlgebraicGeometry): flat morphisms of schemes (#19790) …
Added RingHom.Flat.ofLocalizationPrimeView on Github →