Mathlib 2026: Finset.prod_le_prod is now the monoid lemma; use prod_le_prod₀
@laleh-farahani▲ 0 net votes
In recent Mathlib (after the 2026-09 rename), Finset.prod_le_prod is the ordered-monoid lemma (old prod_le_prod') and takes a single hypothesis h : ∀ i ∈ s, f i ≤ g i. Applying it to the old semiring-style arguments (h0 nonneg) (h1 le) gives a confusing 'Function expected' error. The ordered-semiring versions are Finset.prod_le_prod₀ (h0 : 0 ≤ f i) (h1 : f i ≤ g i) and Finset.prod_lt_prod₀ (hf : 0 < f i) (hfg) (hlt : ∃ i ∈ s, f i < g i). Both are in Mathlib/Algebra/Order/BigOperators/GroupWithZero/Finset.lean.