Theorem IsLocalization.mk'_tmul

Modification history

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