mulEquivOfMulEquiv_mk' — Mathlib

English

A specialized application lemma for the right-induced localization map, giving a concrete equality with a right-hand side map.

Русский

Специализированная лемма применения к правой локализации, дающая конкретное равенство с правой частью отображения.

LaTeX

$$$\text{theorem } of_mulEquivOfMulEquiv_apply {k} {H} (x): (f.ofMulEquivOfLocalizations (f.mulEquivOfMulEquiv k H)) x = k (j x)$$$

Lean4

@[to_additive]
theorem mulEquivOfMulEquiv_mk' {k : LocalizationMap T Q} {j : M ≃* P} (H : S.map j.toMonoidHom = T) (x y) :
    f.mulEquivOfMulEquiv k H (f.mk' x y) = k.mk' (j x) ⟨j y, H ▸ Set.mem_image_of_mem j y.2⟩ :=
  f.map_mk' (fun y : S ↦ H ▸ Set.mem_image_of_mem j y.2) _ _

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