instNonUnitalAlgHomClass

Mathlib.Algebra.Star.StarAlgHom

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

← MathLib Explorer

English

NonUnitalStarAlgHom forms a NonUnitalAlgHomClass.

Русский

NonUnitalStarAlgHom образует класс гомоморфизмов без единицы.

LaTeX

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

Lean4

instance : NonUnitalAlgHomClass (A →⋆ₙₐ[R] B) R A B
    where
  map_smulₛₗ f := f.map_smul'
  map_add f := f.map_add'
  map_zero f := f.map_zero'
  map_mul f := f.map_mul'

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

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

Разделы

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

Аффилиация

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