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 leanprover-community/mathlib4#2120

src/algebra/big_operators/order.lean

@@ -536,6 +536,21 @@ section canonically_ordered_comm_semiring
 
 variables [canonically_ordered_comm_semiring R] {f g h : ι → R} {s : finset ι} {i : ι}
 
+@[simp]
+lemma _root_.canonically_ordered_comm_semiring.multiset_prod_pos [nontrivial R] {m : multiset R} :
+  0 < m.prod ↔ (∀ x ∈ m, (0 : R) < x) :=
+begin
+  induction m using quotient.induction_on,
+  rw [multiset.quot_mk_to_coe, multiset.coe_prod],
+  exact canonically_ordered_comm_semiring.list_prod_pos,
+end
+
+/-- Note that the name is to match `canonically_ordered_comm_semiring.mul_pos`. -/
+@[simp]
+lemma _root_.canonically_ordered_comm_semiring.prod_pos [nontrivial R] :
+  0 < ∏ i in s, f i ↔ (∀ i ∈ s, (0 : R) < f i) :=
+canonically_ordered_comm_semiring.multiset_prod_pos.trans $ by simp
+
 lemma prod_le_prod' (h : ∀ i ∈ s, f i ≤ g i) :
   ∏ i in s, f i ≤ ∏ i in s, g i :=
 begin

src/data/list/big_operators/basic.lean

@@ -486,6 +486,16 @@ begin
     exact mul_pos (h _ $ mem_cons_self _ _) (ih $ λ a ha, h a $ mem_cons_of_mem _ ha) }
 end
 
+/-- A variant of `list.prod_pos` for `canonically_ordered_comm_semiring`. -/
+@[simp]
+lemma _root_.canonically_ordered_comm_semiring.list_prod_pos
+  {α : Type*} [canonically_ordered_comm_semiring α] [nontrivial α] :
+    Π {l : list α}, 0 < l.prod ↔ (∀ x ∈ l, (0 : α) < x)
+| [] := ⟨λ h x hx, hx.elim, λ _, zero_lt_one⟩
+| (x :: xs) := by simp_rw [prod_cons, mem_cons_iff, forall_eq_or_imp,
+    canonically_ordered_comm_semiring.mul_pos,
+    _root_.canonically_ordered_comm_semiring.list_prod_pos]
+
 /-!
 Several lemmas about sum/head/tail for `list ℕ`.
 These are hard to generalize well, as they rely on the fact that `default ℕ = 0`.