instCoeTCStarAlgHom

Mathlib.Algebra.Star.StarAlgHom

URI: https://scilib.ai/kg/mathlib#StarAlgHomClass.instCoeTCStarAlgHom

English

StarAlgHomClass provides that a StarAlgHom is an AlgHom.

Русский

StarAlgHomClass обеспечивает, что StarAlgHom является AlgHom.

LaTeX

$$Each f : A →⋆ₐ[R] B has algebra-hom properties$$

Lean4

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

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

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

Разделы

Аффилиация

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