mathlib

8e44b9f1 - feat(algebra/big_operators): `prod_apply_dite` and `prod_dite` (#3110)

feat(algebra/big_operators): `prod_apply_dite` and `prod_dite` (#3110) Generalize `prod_apply_ite` and `prod_ite` to dependent if-then-else. Since the proofs require `prod_attach`, it needed to move to an earlier line. Zulip discussion: https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/prod_ite_eq