mulEquivOfLocalizations_right_inv

English

For a localization map f and a localization k, the composite f.ofMulEquivOfLocalizations (f.mulEquivOfLocalizations k) equals k; i.e., the constructed map acts as a right inverse to the localization correspondence.

Русский

Для локализационного отображения f и локализации k композиция f.ofMulEquivOfLocalizations (f.mulEquivOfLocalizations k) равна k; то есть построенная карта является правым обратным отображением локализации.

LaTeX

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

Lean4

@[to_additive addEquivOfLocalizations_right_inv]
theorem mulEquivOfLocalizations_right_inv (k : LocalizationMap S P) :
    f.ofMulEquivOfLocalizations (f.mulEquivOfLocalizations k) = k :=
  toMonoidHom_injective <| f.lift_comp k.map_units

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