mathlib

ad5edeb5 - feat(algebra/big_operators): prod_ite_irrel (#14142)

feat(algebra/big_operators): prod_ite_irrel (#14142) A few missing lemams in `big_operators/basic.lean`. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>