trans_toBialgHom — Mathlib

English

The bialgebra hom part of the transitive composition equals the composition of the hom parts.

Русский

Гомоморфная часть композиции через транзитивность равна композиции гомоморфной частей.

LaTeX

$$$((e_{12}.trans e_{23})^{\\mathrm{toAlg}}) = (e_{23}^{\\mathrm{toAlg}})\\circ (e_{12}^{\\mathrm{toAlg}})$$$

Lean4

@[simp]
theorem trans_toBialgHom : (e₁₂.trans e₂₃ : A →ₐc[R] C) = (e₂₃ : B →ₐc[R] C).comp e₁₂ :=
  rfl

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