feat(algebra/big_operators/finprod): add finprod_eq_of_bijective (#10048

)

src/algebra/big_operators/finprod.lean

@@ -619,7 +619,8 @@ finprod_mem_range' (hg.inj_on _)
 
 /-- The product of `f i` over `s : set α` is equal to the product of `g j` over `t : set β`
 if there exists a function `e : α → β` such that `e` is bijective from `s` to `t` and for all
-`x` in `s` we have `f x = g (e x)`. -/
+`x` in `s` we have `f x = g (e x)`.
+See also `finset.prod_bij`. -/
 @[to_additive] lemma finprod_mem_eq_of_bij_on {s : set α} {t : set β} {f : α → M} {g : β → M}
   (e : α → β) (he₀ : set.bij_on e s t) (he₁ : ∀ x ∈ s, f x = g (e x)) :
   ∏ᶠ i ∈ s, f i = ∏ᶠ j ∈ t, g j :=
@@ -628,6 +629,22 @@ begin
   exact finprod_mem_congr rfl he₁
 end
 
+/-- The product of `f i` is equal to the product of `g j` if there exists a bijective function
+`e : α → β` such that for all `x` we have `f x = g (e x)`.
+See `finprod_comp`, `fintype.prod_bijective` and `finset.prod_bij` -/
+@[to_additive] lemma finprod_eq_of_bijective {f : α → M} {g : β → M}
+  (e : α → β) (he₀ : function.bijective e) (he₁ : ∀ x, f x = g (e x)) :
+  ∏ᶠ i, f i = ∏ᶠ j, g j :=
+begin
+  rw [← finprod_mem_univ f, ← finprod_mem_univ g],
+  exact finprod_mem_eq_of_bij_on _ (bijective_iff_bij_on_univ.mp he₀) (λ x _, he₁ x),
+end
+
+/-- Given a bijective function `e` the product of `g i` is equal to the product of `g (e i)`.
+See also `finprod_eq_of_bijective`, `fintype.prod_bijective` and `finset.prod_bij` -/
+@[to_additive] lemma finprod_comp {g : β → M} (e : α → β) (he₀ : function.bijective e) :
+  ∏ᶠ i, g (e i) = ∏ᶠ j, g j := finprod_eq_of_bijective e he₀ (λ x, rfl)
+
 @[to_additive] lemma finprod_set_coe_eq_finprod_mem (s : set α) : ∏ᶠ j : s, f j = ∏ᶠ i ∈ s, f i :=
 begin
   rw [← finprod_mem_range, subtype.range_coe],