ofMulEquivOfDom_comp_symm — Mathlib

English

Let f be a localization map for S and k the isomorphism P ≃* M with T.map k = S. Then for every x in M, f.ofMulEquivOfDom H (k.symm x) = f x, where H encodes T.map k = S.

Русский

Пусть f — локализационная карта для S и k — изоморфизм P ≃* M с условием T.map k = S. Тогда для каждого x ∈ M верно f.ofMulEquivOfDom H (k.symm x) = f x, где H кодирует T.map k = S.

LaTeX

$$$\forall x,\ f.ofMulEquivOfDom(H)(k.symm\, x) = f\,x,$ где $H$ задаёт $T.map k.toMonoidHom = S$.$$

Lean4

@[to_additive]
theorem ofMulEquivOfDom_comp_symm {k : P ≃* M} (H : T.map k.toMonoidHom = S) (x) :
    f.ofMulEquivOfDom H (k.symm x) = f x :=
  congr_arg f <| k.apply_symm_apply x

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