instFunLike

Mathlib.RingTheory.Bialgebra.Equiv

URI: https://scilib.ai/kg/mathlib#BialgEquiv.instFunLike

English

The FunLike instance for BialgEquiv is declared.

Русский

Объявлен экземпляр FunLike для BialgEquiv.

LaTeX

$$$\\text{instance } : FunLike (A \\simeq_{bialg} B) A B$$$

Lean4

instance : FunLike (A ≃ₐc[R] B) A B where
  coe := DFunLike.coe
  coe_injective' := DFunLike.coe_injective

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

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

Разделы

Аффилиация

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