mulEquivOfMulEquiv_eq — Mathlib

English

If a certain equality of localized maps holds, then the induced equality on monoid homomorphisms follows.

Русский

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

LaTeX

$$$f.mulEquivOfMulEquiv k H).toMonoidHom = f.map \_ k$$$

Lean4

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

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