sum_antidiagonal_succ

Mathlib.Algebra.BigOperators.NatAntidiagonal

URI: https://scilib.ai/kg/mathlib#Finset.Nat.sum_antidiagonal_succ

← MathLib Explorer

English

For the Nat version,

Русский

Для натуральных чисел аналогично:

LaTeX

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

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru