comp_mul — Mathlib

English

Composition distributes over product of Monoid Homomorphisms: g ∘ (f1 · f2) = (g ∘ f1) · (g ∘ f2).

Русский

Компоновка сохраняет произведение гомоморфизмов монады: g ∘ (f1 · f2) = (g ∘ f1) · (g ∘ f2).

LaTeX

$$$g\circ (f_1 * f_2) = (g \circ f_1) * (g \circ f_2)$$$

Lean4

@[to_additive]
theorem comp_mul [Mul M] [CommSemigroup N] [CommSemigroup 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]

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