instCoeToCoalgHom

Mathlib.RingTheory.Coalgebra.Hom

URI: https://scilib.ai/kg/mathlib#CoalgHomClass.instCoeToCoalgHom

English

There is a default coercion from any F with CoalgHomClass to a coalgebra hom.

Русский

Существует стандартное приведение из любого F с CoalgHomClass к коалгебраическому гомоморфизму.

LaTeX

$$$\\text{instCoeToCoalgHom} : F \\Rightarrow (A \\to_{R}^{coalg} B)$$$

Lean4

instance instCoeToCoalgHom : CoeHead F (A →ₗc[R] B) :=
  ⟨CoalgHomClass.toCoalgHom⟩

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

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

Разделы

Аффилиация

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