Theorem RingHom.OfLocalizationSpan.ofIsLocalization'

Modification history

2024-11-01 10:29
Mathlib/RingTheory/LocalProperties/Basic.lean
feat(AlgebraicGeometry/Morphisms): affine + ring hom property (#18356) …
Added RingHom.OfLocalizationSpan.ofIsLocalization'View on Github →