prod_antidiagonal_succ' — Mathlib

English

For any n and f: ℕ×ℕ → M,

Русский

Для любых n и f: ℕ×ℕ → M:

LaTeX

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

Lean4

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

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