feat(algebra/big_operators): prod_comp (#2594)
feat(algebra/big_operators): prod_comp (#2594)

This is a lemma that @jcommelin looks like he could have used in Chevalley Warning, and is probably useful elsewhere.



leanprover-community/mathlib,leanprover-community/mathlib