sum_add_index — Mathlib

English

If f(i,0)=0 for all i and f(a, b1+b2) = f(a,b1) + f(a,b2), then (p+q).sum f = p.sum f + q.sum f.

Русский

Если f(i,0)=0 и f(a, b1+b2) = f(a,b1) + f(a,b2), тогда (p+q).sum f = p.sum f + q.sum f.

LaTeX

$$$ (p+q).sum f = p.sum f + q.sum f$ \text{under } (\forall i, f i 0 = 0) \text{ and } (\forall a,b, f a (b_1 + b_2) = f a b_1 + f a b_2)$$$

Lean4

theorem sum_add_index {S : Type*} [AddCommMonoid S] (p q : R[X]) (f : ℕ → R → S) (hf : ∀ i, f i 0 = 0)
    (h_add : ∀ a b₁ b₂, f a (b₁ + b₂) = f a b₁ + f a b₂) : (p + q).sum f = p.sum f + q.sum f :=
  by
  rw [show p + q = ⟨p.toFinsupp + q.toFinsupp⟩ from add_def p q]
  exact Finsupp.sum_add_index (fun i _ ↦ hf i) (fun a _ b₁ b₂ ↦ h_add a b₁ b₂)

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