Commit 2023-02-06 23:03 bb37dbda

feat(algebra/big_operators/order): prod_pos lemma for ennreal (#18391) This adds:

• canonically_ordered_comm_semiring.list_prod_pos
• canonically_ordered_comm_semiring.multiset_prod_pos
• canonically_ordered_comm_semiring.prod_pos which extend the existing canonically_ordered_comm_semiring.mul_pos. Primarily, these are intended for use on enat and ennreal, which don't satisfy the typeclasses required by list.prod_pos and finset.prod_pos. At any rate, those statements are weaker. Forward port in https://github.com/leanprover-community/mathlib4/pull/2120