sum_congr — Mathlib

English

If two families g1, g2 agree termwise on the support of f, then their sums against f are equal.

Русский

Если две семейства g1, g2 согласны покомпонентно на поддержке f, то их суммы против f равны.

LaTeX

$$$$ f.sum g_1 = f.sum g_2 \quad \text{whenever } \forall x \in f.\text{support},\; g_1 x (f.coeff x) = g_2 x (f.coeff x) $$$$

Lean4

theorem sum_congr {f : SkewMonoidAlgebra k G} {M : Type*} [AddCommMonoid M] {g₁ g₂ : G → k → M}
    (h : ∀ x ∈ f.support, g₁ x (f.coeff x) = g₂ x (f.coeff x)) : f.sum g₁ = f.sum g₂ :=
  Finset.sum_congr rfl h

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