Theorems · Theorem · category theory

CommBialgCat.ofHom_comp

∀ {R : Type u} [inst : CommRing R] {X Y Z : Type v} [inst_1 : CommRing X] [inst_2 : Bialgebra R X] [inst_3 : CommRing Y]
  [inst_4 : Bialgebra R Y] [inst_5 : CommRing Z] [inst_6 : Bialgebra R Z] (f : X →ₐc[R] Y) (g : Y →ₐc[R] Z),
  CommBialgCat.ofHom (g.comp f) = CategoryTheory.CategoryStruct.comp (CommBialgCat.ofHom f) (CommBialgCat.ofHom g)

Defined in

Mathlib.Algebra.Category.CommBialgCat

Cited by

0 results in Mathlib

Foundations

Depth 76 from the axioms · uses propext, Quot.sound

Assumes

CommRingCommRingBialgebraCommRingBialgebraCommRingBialgebra