sum_zero — Mathlib

English

Let f be an element of a Skew Monoid Algebra. The total sum of the zero-valued coefficients is 0, i.e. summing the zero function yields the zero element.

Русский

Пусть f принадлежит Skew Monoid Algebra. Общая сумма нулевых коэффициентов равна нулю, то есть сумма функции, равной нулю, равна нулю.

LaTeX

$$$ (f.sum\\ (\\lambda a\\,\\lambda b\\: 0)) = 0 $$$

Lean4

@[simp]
theorem sum_zero {N : Type*} [AddCommMonoid N] {f : SkewMonoidAlgebra k G} : (f.sum fun _ _ ↦ (0 : N)) = 0 :=
  Finset.sum_const_zero

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