coe_comp_monoidHom — Mathlib

English

Let f: β →*o γ and g: α →*o β be order-preserving monoid homomorphisms. The underlying function of the composite equals the composition of the underlying functions: (f.comp g) as a function equals (f : β →* γ).comp g.

Русский

Пусть f: β →*o γ и g: α →*o β — упорядоченные моноид-гомоморфизмы. Тогда отображение, полученное как композиция f с g, совпадает с композицией их базовых отображений на уровне функций.

LaTeX

$$$ (f.comp g : α \to* γ) = (f : β \to* γ).comp g $$$

Lean4

@[to_additive]
theorem coe_comp_monoidHom (f : β →*o γ) (g : α →*o β) : (f.comp g : α →* γ) = (f : β →* γ).comp g :=
  rfl

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