comp_coprod — Mathlib

English

Let h: P →* Q be a monoid homomorphism and f: M →* P, g: N →* P be monoid homomorphisms. Then h ∘ (f.coprod g) = (h ∘ f) coprod (h ∘ g).

Русский

Пусть h: P →* Q и f: M →* P, g: N →* P — моноид-гомоморфизмы. Тогда h ∘ (f.coprod g) = (h ∘ f) coprod (h ∘ g).

LaTeX

$$$h \\circ (f \\coprod g) = (h \\circ f) \\coprod (h \\circ g).$$$

Lean4

@[to_additive]
theorem comp_coprod {Q : Type*} [CommMonoid Q] (h : P →* Q) (f : M →* P) (g : N →* P) :
    h.comp (f.coprod g) = (h.comp f).coprod (h.comp g) :=
  ext fun x => by simp

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