toBialgHom_comp — Mathlib

English

The operation of turning a HopfAlgCat morphism into a BialgHom is compatible with composition: (f ≫ g).toBialgHom = g.toBialgHom ∘ f.toBialgHom.

Русский

Преобразование морфизма HopfAlgCat в BialgHom совместимо с композицией: (f ≫ g).toBialgHom = g.toBialgHom ∘ f.toBialgHom.

LaTeX

$$$(f \gg g).toBialgHom = g.toBialgHom.comp f.toBialgHom$$$

Lean4

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

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