Commit 2026-08-31 10:08 83377d00

View on Github →

feat(Algebra/Order): maximally varying version of prod_le_prod_of_subset_of_one_le (#39646) We need this for gcongr.

Estimated changes

Modified Mathlib/Algebra/Order/BigOperators/GroupWithZero/Finset.lean

modified theorem Finset.prod_le_prod_of_subset_of_le_one

modified theorem Finset.prod_le_prod_of_subset_of_one_le

added theorem Finset.prod_mono_of_subset_of_le_one₀

added theorem Finset.prod_mono_of_subset_of_one_le₀

Modified Mathlib/Analysis/Complex/Exponential.lean