feat(algebra/big_operators): split products and sums over fin (a+b) (#…

…13291)




Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>

src/algebra/big_operators/basic.lean

@@ -343,6 +343,26 @@ begin
     cases H }
 end
 
+@[simp, to_additive]
+lemma prod_on_sum [fintype α] [fintype γ] (f : α ⊕ γ → β) :
+  ∏ (x : α ⊕ γ), f x  =
+    (∏ (x : α), f (sum.inl x)) * (∏ (x : γ), f (sum.inr x)) :=
+begin
+  haveI := classical.dec_eq (α ⊕ γ),
+  convert prod_sum_elim univ univ (λ x, f (sum.inl x)) (λ x, f (sum.inr x)),
+  { ext a,
+    split,
+    { intro x,
+      cases a,
+      { simp only [mem_union, mem_map, mem_univ, function.embedding.inl_apply, or_false,
+          exists_true_left, exists_apply_eq_apply, function.embedding.inr_apply, exists_false], },
+      { simp only [mem_union, mem_map, mem_univ, function.embedding.inl_apply, false_or,
+          exists_true_left, exists_false, function.embedding.inr_apply,
+          exists_apply_eq_apply], }, },
+    { simp only [mem_univ, implies_true_iff], }, },
+  { simp only [sum.elim_comp_inl_inr], },
+end
+
 @[to_additive]
 lemma prod_bUnion [decidable_eq α] {s : finset γ} {t : γ → finset α}
   (hs : set.pairwise_disjoint ↑s t) :

src/algebra/big_operators/fin.lean

@@ -6,6 +6,7 @@ Authors: Yury Kudryashov, Anne Baanen
 import algebra.big_operators.basic
 import data.fintype.fin
 import data.fintype.card
+import logic.equiv.fin
 /-!
 # Big operators and `fin`
 
@@ -113,6 +114,29 @@ lemma prod_filter_succ_lt {M : Type*} [comm_monoid M] {n : ℕ} (j : fin n) (v :
     ∏ j in univ.filter (λ i, j < i), v j.succ :=
 by rw [univ_filter_succ_lt, finset.prod_map, rel_embedding.coe_fn_to_embedding, coe_succ_embedding]
 
+@[to_additive]
+lemma prod_congr' {M : Type*} [comm_monoid M] {a b : ℕ} (f : fin b → M) (h : a = b) :
+  ∏ (i : fin a), f (cast h i) = ∏ (i : fin b), f i :=
+by { subst h, congr, ext, congr, ext, rw coe_cast, }
+
+@[to_additive]
+lemma prod_univ_add {M : Type*} [comm_monoid M] {a b : ℕ} (f : fin (a+b) → M) :
+  ∏ (i : fin (a+b)), f i =
+  (∏ (i : fin a), f (cast_add b i)) * ∏ (i : fin b), f (nat_add a i) :=
+begin
+  rw fintype.prod_equiv fin_sum_fin_equiv.symm f (λ i, f (fin_sum_fin_equiv.to_fun i)), swap,
+  { intro x,
+    simp only [equiv.to_fun_as_coe, equiv.apply_symm_apply], },
+  apply prod_on_sum,
+end
+
+@[to_additive]
+lemma prod_trunc {M : Type*} [comm_monoid M] {a b : ℕ} (f : fin (a+b) → M)
+  (hf : ∀ (j : fin b), f (nat_add a j) = 1) :
+  ∏ (i : fin (a+b)), f i =
+  ∏ (i : fin a), f (cast_le (nat.le.intro rfl) i) :=
+by simpa only [prod_univ_add, fintype.prod_eq_one _ hf, mul_one]
+
 end fin
 
 namespace list