toAddMonoidAlgebra

Mathlib.Algebra.MonoidAlgebra.ToDirectSum

URI: https://scilib.ai/kg/mathlib#DirectSum.toAddMonoidAlgebra

Lean4

/-- Interpret a homogeneous `DirectSum` as an `AddMonoidAlgebra`. -/
def toAddMonoidAlgebra (f : ⨁ _ : ι, M) : AddMonoidAlgebra M ι :=
  DFinsupp.toFinsupp f

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

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

Разделы

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

Аффилиация

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