id_toCoalgHom

Mathlib.RingTheory.Bialgebra.Hom

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

English

The identity bialg homomorphism coincides with the identity algebra homomorphism.

Русский

Идентичный гомоморфизм биналгомов совпадает с идентичным алгомоморфизмом.

LaTeX

$$$\\mathrm{id}_{\\mathrm{BialgHom}}\\; R\\; A = \\mathrm{id}_{\\mathrm{AlgHom}}(R,A)$$$

Lean4

@[simp]
theorem id_toCoalgHom : BialgHom.id R A = CoalgHom.id R A :=
  rfl

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

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

Разделы

Аффилиация

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