instAlgHomClass

Mathlib.Algebra.Star.StarAlgHom

URI: https://scilib.ai/kg/mathlib#StarAlgHom.instAlgHomClass

← MathLib Explorer

English

StarAlgHomClass provides that a StarAlgHom is an AlgHom for all types A,B.

Русский

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

LaTeX

$$instance : AlgHomClass (A →⋆ₐ[R] B) R A B$$

Lean4

instance : AlgHomClass (A →⋆ₐ[R] B) R A B where
  map_mul f := f.map_mul'
  map_one f := f.map_one'
  map_add f := f.map_add'
  map_zero f := f.map_zero'
  commutes f := f.commutes'

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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