comp_assoc — Mathlib

English

Composition of OneHom is associative: composing f,g,h yields the same as (h ∘ g) ∘ f = h ∘ (g ∘ f).

Русский

Компоновка OneHom ассоциативна: (h ∘ g) ∘ f = h ∘ (g ∘ f).

LaTeX

$$$ (h \\circ g) \\circ f = h \\circ (g \\circ f) $$$

Lean4

/-- Composition of monoid homomorphisms is associative. -/
@[to_additive /-- Composition of additive monoid homomorphisms is associative. -/
    ]
theorem comp_assoc {Q : Type*} [One M] [One N] [One P] [One Q] (f : OneHom M N) (g : OneHom N P) (h : OneHom P Q) :
    (h.comp g).comp f = h.comp (g.comp f) :=
  rfl

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