instCoeTCNonUnitalStarAlgHomOfStarHomClass

Mathlib.Algebra.Star.StarAlgHom

URI: https://scilib.ai/kg/mathlib#NonUnitalStarAlgHomClass.instCoeTCNonUnitalStarAlgHomOfStarHomClass

English

If F is a StarHomClass, then F forms a CoeTC to NonUnitalStarAlgHom.

Русский

Если F — StarHomClass, то F образует отображение сопряжённости в NonUnitalStarAlgHom.

LaTeX

$$$\forall F\;\big(\text{StarHomClass } F\; A\; B\big) \Rightarrow \text{CoeTC } F\; (A\; B) $$$

Lean4

instance [StarHomClass F A B] : CoeTC F (A →⋆ₙₐ[R] B) :=
  ⟨toNonUnitalStarAlgHom⟩

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

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

Разделы

Аффилиация

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