Commit 2025-05-21 12:47 b37ece24
View on Github →feat(RingTheory/LocalProperties): constructor for RingHom.OfLocalizationSpan (#22933)
Adds a constructor for RingHom.OfLocalizationSpan where P (algebraMap (Localization.Away r) (Localization.Away r ⊗[R] S)) has to be shown for a covering family. This is convenient in practice, because the base change API is the more generally applicable framework.
<!-- The text above the `