toDirectSum_one

Mathlib.Algebra.MonoidAlgebra.ToDirectSum

URI: https://scilib.ai/kg/mathlib#AddMonoidAlgebra.toDirectSum_one

English

The direct sum of the unit element 1 in AddMonoidAlgebra is the unit in DirectSum.

Русский

На DirectSum единица соответствует единице в AddMonoidAlgebra.

LaTeX

$$$\\bigl(1 : AddMonoidAlgebra M ι\\bigr).toDirectSum = 1$$$

Lean4

@[simp]
theorem toDirectSum_one [DecidableEq ι] [Zero ι] [Semiring M] : (1 : AddMonoidAlgebra M ι).toDirectSum = 1 :=
  Finsupp.toDFinsupp_single _ _

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

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

Разделы

Аффилиация

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