instFunLike

Mathlib.Algebra.Star.StarAlgHom

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

English

The function-like structure is canonical for NonUnitalStarAlgHom.

Русский

Функциональная аналогия задана канонически для NonUnitalStarAlgHom.

LaTeX

$$$\text{instance } [\text{FunLike } (A \to⋆ₙₐ[R] B) A B]$$$

Lean4

instance : FunLike (A →⋆ₙₐ[R] B) A B where
  coe f := f.toFun
  coe_injective' := by rintro ⟨⟨⟨⟨f, _⟩, _⟩, _⟩, _⟩ ⟨⟨⟨⟨g, _⟩, _⟩, _⟩, _⟩ h; congr

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

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

Разделы

Аффилиация

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