addMonoidHom_comp — Mathlib

English

Composition of mapDomain along f and g equals mapDomain along f ∘ g.

Русский

Сложение mapDomain по f и по g эквивалентно mapDomain по f ∘ g.

LaTeX

$$$\\operatorname{mapDomain.addMonoidHom} (f \\circ g) = (\\operatorname{mapDomain.addMonoidHom} f) \\cdot (\\operatorname{mapDomain.addMonoidHom} g).$$$

Lean4

theorem addMonoidHom_comp (f : β → γ) (g : α → β) :
    (mapDomain.addMonoidHom (f ∘ g) : (α →₀ M) →+ γ →₀ M) =
      (mapDomain.addMonoidHom f).comp (mapDomain.addMonoidHom g) :=
  AddMonoidHom.ext fun _ => mapDomain_comp

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