From 4036212231d22c77f5480ce7e53c1d8f066e11f0 Mon Sep 17 00:00:00 2001
From: "Yury G. Kudryashov" <urkud@urkud.name>
Date: Mon, 26 Oct 2020 04:25:05 +0000
Subject: [PATCH] feat(algebra/big_operators/nat_antidiagonal): a few more
 lemmas (#4783)

---
 .../big_operators/nat_antidiagonal.lean       | 34 ++++++++++++++++---
 1 file changed, 29 insertions(+), 5 deletions(-)

diff --git a/src/algebra/big_operators/nat_antidiagonal.lean b/src/algebra/big_operators/nat_antidiagonal.lean
index 4abb48d4be222..cb274d2f3fc63 100644
--- a/src/algebra/big_operators/nat_antidiagonal.lean
+++ b/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