antidiagonal_succ' — Mathlib

English

A variant of the succ recursion for the antidiagonal that also shifts the second component to 0.

Русский

Вариант рекурсии по антидиагонали с добавлением (n+1,0) снизу.

LaTeX

$$$\\mathrm{antidiagonal}(n+1) = (n+1,0) \\;\\uplus\\; \\mathrm{antidiagonal}(n).\\mathrm{map}(\\mathrm{Prod.map}(\\mathrm{id}, \\mathrm{Nat.succ})).$$$

Lean4

theorem antidiagonal_succ' {n : ℕ} :
    antidiagonal (n + 1) = (n + 1, 0) ::ₘ (antidiagonal n).map (Prod.map id Nat.succ) := by
  rw [antidiagonal, List.Nat.antidiagonal_succ', ← coe_add, Multiset.add_comm, antidiagonal, map_coe, coe_add,
    List.singleton_append, cons_coe]

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