English
Let M, N, P be monoids with P commutative. If f1, f2: M →* N are monoid homomorphisms and g: N →* P is a monoid homomorphism, then the composition with the product equals the product of the compositions: g ∘ (f1 ⋅ f2) = (g ∘ f1) ⋅ (g ∘ f2).
Русский
Пусть M, N, P — моноиды и P коммутативен. Если f1, f2: M →* N — моноид-гомоморфизмы, и g: N →* P — моноид-гомоморфизм, то композиция с произведением равна произведению композиций: g ∘ (f1 ⋅ f2) = (g ∘ f1) ⋅ (g ∘ f2).
LaTeX
$$$ g \\circ (f_1 \\cdot f_2) = (g \\circ f_1) \\cdot (g \\circ f_2) $$$
Lean4
@[to_additive]
theorem comp_mul [CommMonoid P] (g : N →* P) (f₁ f₂ : M →* N) : g.comp (f₁ * f₂) = g.comp f₁ * g.comp f₂ := by ext;
simp only [mul_apply, Function.comp_apply, map_mul, coe_comp]
