mulEquivOfMulEquiv_eq_map — Mathlib

English

A specialized map equality under composition with an isomorphism leads to an equality of monoid homomorphisms.

Русский

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

LaTeX

$$$(f.mulEquivOfMulEquiv k H).toMonoidHom (f.map ? k) = f.map ? k$$$

Lean4

@[to_additive]
theorem mulEquivOfMulEquiv_eq_map {k : LocalizationMap T Q} {j : M ≃* P} (H : S.map j.toMonoidHom = T) :
    (f.mulEquivOfMulEquiv k H).toMonoidHom =
      f.map (fun y : S ↦ show j.toMonoidHom y ∈ T from H ▸ Set.mem_image_of_mem j y.2) k :=
  rfl

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