English
Let f: M →* P, g: N →* P and h: P →* Q be monoid homomorphisms. Then the composition with the coproduct satisfies h ∘ (f ∘ g) = (h ∘ f) ∘ (h ∘ g); equivalently, h(f(m)·g(n)) = h(f(m))·h(g(n)) for all m ∈ M, n ∈ N.
Русский
Пусть f: M →* P и g: N →* P, а также h: P →* Q — гомоморфизмы моноидов. Тогда композиция с копродуктом распределяется: h ∘ (f.coprod g) = (h ∘ f).coprod (h ∘ g); то есть для всех m ∈ M, n ∈ N выполняется h(f(m) g(n)) = h(f(m)) h(g(n)).
LaTeX
$$$ h \\circ (f \\coprod g) = (h \\circ f) \\coprod (h \\circ g) $$$
Lean4
@[to_additive]
theorem comp_coprod {Q : Type*} [CommSemigroup 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
