feat(algebra/big_operators): prod_dite_eq (#3167)
Add `finset.prod_dite_eq`, the dependent analogue of `finset.prod_ite_eq`, and its primed version for the flipped equality.
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
