sum_cons' — Mathlib

English

Variant of sum_cons' for Finset with general f and a condition that f x 0 = 0 for all x.

Русский

Вариант sum_cons' для Finset с условиями на f.

LaTeX

$$$\text{sum}_{{Fin}}(\text{cons } i\, σ) \, f = f(0,i) + \text{sum}(σ, \text{tail} f)$$$

Lean4

theorem sum_cons' [Zero M] [AddCommMonoid N] (n : ℕ) (σ : Fin n →₀ M) (i : M) (f : Fin (n + 1) → M → N)
    (h : ∀ x, f x 0 = 0) : (sum (Finsupp.cons i σ) f) = f 0 i + sum σ (Fin.tail f) :=
  by
  rw [sum_fintype _ _ (fun _ => by apply h), sum_fintype _ _ (fun _ => by apply h)]
  simp_rw [Fin.sum_univ_succ, cons_zero, cons_succ]
  congr

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