Cannot apply Finset.one_le_prod'

Stream: new members

[Zhang Qinchuan]

docs#Finset.one_le_prod' only apply to docs#OrderedCommMonoid , but Real is not OrderedCommMonoid.

import Mathlib
example {f : ℕ → ℝ} {s : Finset ℕ} (h : ∀ i ∈ s, 1 ≤ f i) : 1 ≤ ∏ i ∈ s, f i := by
  exact Finset.one_le_prod' h -- Failed!

It is easy to prove one_le_prod for Real. But I did not find such theorem in Mathlib.

import Mathlib
theorem one_le_prod {R ι: Type*} [LinearOrderedCommRing R] {f : ι → R} {s : Finset ι}
    (h : ∀ i ∈ s, 1 ≤ f i) : 1 ≤ ∏ i ∈ s, f i := calc
  _ = ∏ _ ∈ s, (1 : R) := by simp
  _ ≤ _ := Finset.prod_le_prod (by intros; norm_num) h

example {f : ℕ → ℝ} {s : Finset ℕ} (h : ∀ i ∈ s, 1 ≤ f i) : 1 ≤ ∏ i ∈ s, f i :=
  one_le_prod h