mathlib

ab2c44c4 - feat(algebra/big_operators/ring): add finset.prod_[one_]sub_ordered (#6811)

feat(algebra/big_operators/ring): add finset.prod_[one_]sub_ordered (#6811) Add 2 lemmas useful for partition of unity, `finset.prod_sub_ordered` and `finset.prod_one_sub_ordered`. Also add an explicit `[decidable_eq]` assumption to `finset.induction_on_max` (without it some `rw`s failed).