mulEquivOfLocalizations — Mathlib

English

Equality of localized equivalences.

Русский

Равенство локализованных эквивалентностей.

LaTeX

$$$ f.mulEquivOfLocalizations (f.ofMulEquivOfLocalizations k) = k $$$

Lean4

/-- If `f : M →* N` and `k : M →* P` are Localization maps for a Submonoid `S`, we get an
isomorphism of `N` and `P`. -/
@[to_additive /-- If `f : M →+ N` and `k : M →+ R` are Localization maps for an AddSubmonoid `S`, we get an
    isomorphism of `N` and `R`. -/
    ]
noncomputable def mulEquivOfLocalizations (k : LocalizationMap S P) : N ≃* P :=
  { toFun := f.lift k.map_units
    invFun := k.lift f.map_units
    left_inv := f.lift_left_inverse
    right_inv := k.lift_left_inverse
    map_mul' := MonoidHom.map_mul _ }

Похожие утверждения