of_mulEquivOfMulEquiv_apply — Mathlib

English

A core compatibility statement for how the composed localization maps relate under a domain isomorphism.

Русский

Главное утверждение о том, как локализационные отображения ведут себя под изоморфизмом домена.

LaTeX

$$$f.ofMulEquivOfLocalizations (f.mulEquivOfMulEquiv k H) = k.ofMulEquivOfDom H$$$

Lean4

@[to_additive]
theorem of_mulEquivOfMulEquiv_apply {k : LocalizationMap T Q} {j : M ≃* P} (H : S.map j.toMonoidHom = T) (x) :
    f.ofMulEquivOfLocalizations (f.mulEquivOfMulEquiv k H) x = k (j x) :=
  Submonoid.LocalizationMap.ext_iff.1 (f.mulEquivOfLocalizations_right_inv (k.ofMulEquivOfDom H)) x

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