sum_monomial_eq — Mathlib

English

For any abelian monoid-valued function b with a certain zero condition at the origin, the sum of C a mapped by b equals b 0 a.

Русский

Для любой функции b, удовлетворяющей условию нуля в начале координат, сумма C a, применяемая к b, равна b 0 a.

LaTeX

$$$\sum (C a) b = b 0 a \quad\text{provided } b 0 0 = 0$$$

Lean4

@[simp]
theorem sum_monomial_eq {A : Type*} [AddCommMonoid A] {u : σ →₀ ℕ} {r : R} {b : (σ →₀ ℕ) → R → A} (w : b u 0 = 0) :
    sum (monomial u r) b = b u r :=
  Finsupp.sum_single_index w

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