comp_mul — Mathlib

English

For IsOrderedMonoid β, IsOrderedMonoid γ and g: β →*o γ, f1, f2: α →*o β, the product of homomorphisms respects composition: g.comp (f1 * f2) = g.comp f1 * g.comp f2.

Русский

Для IsOrderedMonoid β, IsOrderedMonoid γ и гомоморфизма g: β →*o γ, а также f1, f2: α →*o β, произведение гомоморфизмов сохраняет композицию: g.comp (f1 * f2) = g.comp f1 * g.comp f2.

LaTeX

$$$ g.comp (f_1 * f_2) = g.comp f_1 * g.comp f_2 $$$

Lean4

@[to_additive]
theorem comp_mul [IsOrderedMonoid β] [IsOrderedMonoid γ] (g : β →*o γ) (f₁ f₂ : α →*o β) :
    g.comp (f₁ * f₂) = g.comp f₁ * g.comp f₂ :=
  ext fun _ => map_mul g _ _

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