Theorem IsLocalization.tmul_mk'

Modification history

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