Theorem Finset.prod_mono_of_subset_of_le_one₀

Modification history

2026-08-31 10:08
Mathlib/Algebra/Order/BigOperators/GroupWithZero/Finset.lean
feat(Algebra/Order): maximally varying version of `prod_le_prod_of_subset_of_one_le` (#39646) …
Added Finset.prod_mono_of_subset_of_le_one₀View on Github →