mathlib

bb37dbda - feat(algebra/big_operators/order): prod_pos lemma for `ennreal` (#18391)

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