feat(algebra/big_operators/nat_antidiagonal): a few more lemmas (#4783)

src/algebra/big_operators/nat_antidiagonal.lean

@@ -15,20 +15,44 @@ This file contains theorems relevant to big operators over `finset.nat.antidiago
 
 open_locale big_operators
 
-variables {α : Type*} [add_comm_monoid α]
+variables {M N : Type*} [comm_monoid M] [add_comm_monoid N]
 
 namespace finset
 namespace nat
 
-lemma sum_antidiagonal_succ {n : ℕ} {f : ℕ × ℕ → α} :
-  (antidiagonal (n + 1)).sum f = f (0, n + 1) + ((antidiagonal n).map
-  (function.embedding.prod_map ⟨nat.succ, nat.succ_injective⟩ (function.embedding.refl _))).sum f :=
+lemma prod_antidiagonal_succ {n : ℕ} {f : ℕ × ℕ → M} :
+  ∏ p in antidiagonal (n + 1), f p = f (0, n + 1) * ∏ p in antidiagonal n, f (p.1 + 1, p.2) :=
 begin
-  rw [antidiagonal_succ, sum_insert],
+  rw [antidiagonal_succ, prod_insert, prod_map], refl,
   intro con, rcases mem_map.1 con with ⟨⟨a,b⟩, ⟨h1, h2⟩⟩,
   simp only [prod.mk.inj_iff, function.embedding.coe_prod_map, prod.map_mk] at h2,
   apply nat.succ_ne_zero a h2.1,
 end
 
+lemma sum_antidiagonal_succ {n : ℕ} {f : ℕ × ℕ → N} :
+  ∑ p in antidiagonal (n + 1), f p = f (0, n + 1) + ∑ p in antidiagonal n, f (p.1 + 1, p.2) :=
+@prod_antidiagonal_succ (multiplicative N) _ _ _
+
+@[to_additive]
+lemma prod_antidiagonal_swap {n : ℕ} {f : ℕ × ℕ → M} :
+  ∏ p in antidiagonal n, f p.swap = ∏ p in antidiagonal n, f p :=
+by { nth_rewrite 1 ← map_swap_antidiagonal, rw [prod_map], refl }
+
+lemma prod_antidiagonal_succ' {n : ℕ} {f : ℕ × ℕ → M} :
+  ∏ p in antidiagonal (n + 1), f p = f (n + 1, 0) * ∏ p in antidiagonal n, f (p.1, p.2 + 1) :=
+begin
+  rw [← prod_antidiagonal_swap, prod_antidiagonal_succ, ← prod_antidiagonal_swap],
+  refl
+end
+
+lemma sum_antidiagonal_succ' {n : ℕ} {f : ℕ × ℕ → N} :
+  ∑ p in antidiagonal (n + 1), f p = f (n + 1, 0) + ∑ p in antidiagonal n, f (p.1, p.2 + 1) :=
+@prod_antidiagonal_succ' (multiplicative N) _ _ _
+
+@[to_additive]
+lemma prod_antidiagonal_subst {n : ℕ} {f : ℕ × ℕ → ℕ → M} :
+  ∏ p in antidiagonal n, f p n = ∏ p in antidiagonal n, f p (p.1 + p.2) :=
+prod_congr rfl $ λ p hp, by rw [nat.mem_antidiagonal.1 hp]
+
 end nat
 end finset