sum_cons — Mathlib

English

Let n be a natural, σ : Fin n →₀ M, i ∈ M. Then sum of cons i σ over Fin (n+1) equals i plus the sum of σ over Fin.tail f.

Русский

Сумма cons i σ по Fin (n+1) равна i плюс сумма σ по Fin.tail.

LaTeX

$$$\text{sum}(\text{cons } i\, σ) = i + \text{sum}(σ, \text{tail}).$$$

Lean4

theorem sum_cons [AddCommMonoid M] (n : ℕ) (σ : Fin n →₀ M) (i : M) :
    (sum (cons i σ) fun _ e ↦ e) = i + sum σ (fun _ e ↦ e) :=
  by
  rw [sum_fintype _ _ (fun _ => rfl), sum_fintype _ _ (fun _ => rfl)]
  exact Fin.sum_cons i σ

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