Theorem RingHom.OfLocalizationSpan.mk

Modification history

2025-05-21 12:47
Mathlib/RingTheory/LocalProperties/Basic.lean
feat(RingTheory/LocalProperties): constructor for `RingHom.OfLocalizationSpan` (#22933) …
Added RingHom.OfLocalizationSpan.mkView on Github →