prod_antidiagonal_succ — Mathlib

English

Let n be a natural number and f : ℕ×ℕ → N. Then

Русский

Пусть n — натуральное число, и f: ℕ×ℕ → N. Тогда сумма по антидиагонали(n+1) удовлетворяет равенству:

LaTeX

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

Lean4

theorem prod_antidiagonal_succ {n : ℕ} {f : ℕ × ℕ → M} :
    (∏ p ∈ antidiagonal (n + 1), f p) = f (0, n + 1) * ∏ p ∈ antidiagonal n, f (p.1 + 1, p.2) := by
  rw [antidiagonal_succ, prod_cons, prod_map]; rfl

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