Theorem Algebra.isLocalization_iff_isPushout

Modification history

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