sum_antidiagonal_succ' — Mathlib

English

The corresponding sum version for succ' satisfies

Русский

Соответствующая сумма для succ' удовлетворяет

LaTeX

$$$$ \\sum_{p ∈ \\mathrm{antidiagonal}(n+1)} f(p) = f(n+1,0) + \\sum_{p ∈ \\mathrm{antidiagonal}(n)} f(p_1, p_2+1). $$$$

Lean4

theorem sum_antidiagonal_succ' {n : ℕ} {f : ℕ × ℕ → N} :
    (∑ p ∈ antidiagonal (n + 1), f p) = f (n + 1, 0) + ∑ p ∈ antidiagonal n, f (p.1, p.2 + 1) :=
  @prod_antidiagonal_succ' (Multiplicative N) _ _ _

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