hom_ofHom — Mathlib

English

For a BialgHom f:X→Y, the corresponding CommBialgCat morphism of ofHom f has the same underlying hom map: (ofHom f).hom = f.

Русский

Для биалгебраического гомоморфизма f:X→Y соответствующий морфизм CommBialgCat имеет то же основанное отображение: (ofHom f).hom = f.

LaTeX

$$$ (\mathrm{ofHom} f).\mathrm{hom} = f $$$

Lean4

@[simp]
theorem hom_ofHom (f : X →ₐc[R] Y) : (ofHom f).hom = f :=
  rfl

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