feat(Combinatorics/Enumerative/Composition): add lemma about products of embeddings (#37413)

Co-authored-by: Xavier Genereux [xaviergenereux@hotmail.com](mailto:xaviergenereux@hotmail.com)

Author: Paul-Lez

Mathlib/Combinatorics/Enumerative/Composition.lean

@@ -446,6 +446,11 @@ theorem sigma_eq_iff_blocks_eq {c : Σ n, Composition n} {c' : Σ n, Composition
   ext1
   exact H
 
+@[to_additive]
+lemma prod_prod_apply_embedding {A : Type*} [CommMonoid A] (a : Fin n → A) (x : Composition n) :
+    ∏ i, ∏ j, a (x.embedding i j) = ∏ i, a i := by
+  simpa [Finset.prod_sigma', Finset.univ_sigma_univ] using x.blocksFinEquiv.prod_comp a
+
 /-! ### The composition `Composition.ones` -/