coe_toCoalgHom

Mathlib.RingTheory.Bialgebra.Hom

URI: https://scilib.ai/kg/mathlib#BialgHom.coe_toCoalgHom

English

The underlying AlgHom of a BialgHom when viewed as AlgHom is the same as its FunLike representation.

Русский

Базовый AlgHom BialgHom, когда рассматривается как AlgHom, совпадает со своим представлением FunLike.

LaTeX

$$$\\text{coe\\_toAlgHom} (f) : = f$$$

Lean4

@[simp, norm_cast]
theorem coe_toCoalgHom (f : A →ₐc[R] B) : ⇑(f : A →ₗc[R] B) = f :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru