singleAddHom

Mathlib.Algebra.SkewMonoidAlgebra.Basic

URI: https://scilib.ai/kg/mathlib#SkewMonoidAlgebra.singleAddHom

Lean4

/-- `single` as an `AddMonoidHom`.

See `lsingle` for the stronger version as a linear map. -/
@[simps]
def singleAddHom (a : G) : k →+ SkewMonoidAlgebra k G
    where
  toFun := single a
  map_zero' := single_zero a
  map_add' _ := single_add a _

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

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

Разделы

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

Аффилиация

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