toDirectSum_zero

Mathlib.Algebra.MonoidAlgebra.ToDirectSum

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

English

The direct sum of the zero AddMonoidAlgebra element is zero.

Русский

Прямой произведение нулевого элемента AddMonoidAlgebra равно нулю.

LaTeX

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

Lean4

@[simp]
theorem toDirectSum_zero [Semiring M] : (0 : AddMonoidAlgebra M ι).toDirectSum = 0 :=
  Finsupp.toDFinsupp_zero

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

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

Разделы

Аффилиация

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