ofMulEquivOfDom_comp — Mathlib

English

Let f be a localization map for S and k: P ≃* M with H: T.map k.toMonoidHom = S. Then f.ofMulEquivOfDom H (k x) = f x for all x ∈ M.

Русский

Пусть f — локализационная карта для S и k: P ≃* M с H: T.map k.toMonoidHom = S. Тогда для всех x ∈ M выполняется f.ofMulEquivOfDom H (k x) = f x.

LaTeX

$$$\forall x,\ f.ofMulEquivOfDom(H)(k x) = f\,x.$$$

Lean4

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

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