Commit 2023-12-04 15:55 fba9b451

feat: (if P then 1 else 0) • a (#8347) Two simple lemmas, smul_ite_zero, and ite_smul_zero. Also delete Finset.sum_univ_ite since it is now provable by simp thanks to these. Rename and turn around the following to match the direction that simp goes in:

• ite_mul_zero_left → ite_zero_mul
• ite_mul_zero_right → mul_ite_zero
• ite_and_mul_zero → ite_zero_mul_ite_zero