toBialgHom_comp — Mathlib

English

The underlying BialgHom respects composition: the BialgHom of a composite morphism equals the composition of the BialgHoms.

Русский

Начальная биалгомоморфия сохраняет композицию: гомоморфизм BialgHom от композиции равен композиции гомоморфов.

LaTeX

$$$ (f \circ g).toBialgHom = g.toBialgHom \circ f.toBialgHom $$$

Lean4

@[simp]
theorem toBialgHom_comp {X Y Z : BialgCat.{v} R} (f : X ⟶ Y) (g : Y ⟶ Z) :
    (f ≫ g).toBialgHom = g.toBialgHom.comp f.toBialgHom :=
  rfl

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