Big operators for nat_antidiagonal
This file contains theorems relevant to big operators over finset.nat.antidiagonal.
theorem
finset.nat.sum_antidiagonal_succ
{α : Type u_1}
[add_comm_monoid α]
{n : ℕ}
{f : ℕ × ℕ → α} :
(finset.nat.antidiagonal (n + 1)).sum f = f (0, n + 1) + (finset.map ({to_fun := nat.succ, inj' := nat.succ_injective}.prod_map (function.embedding.refl ℕ)) (finset.nat.antidiagonal n)).sum f