Commit 2023-09-27 20:27 c8320acc

View on Github →

feat: When the sum of a nonneg function is zero (#7372) Also fix implicitness of arguments to Finset.sum_singleton.

Estimated changes

Modified Mathlib/Algebra/BigOperators/Basic.lean

added theorem Finset.prod_powersetLen

modified theorem Finset.prod_singleton

Modified Mathlib/Algebra/BigOperators/Order.lean

added theorem Fintype.one_le_prod

added theorem Fintype.one_lt_prod

added theorem Fintype.one_lt_prod_iff_of_one_le

added theorem Fintype.prod_eq_one_iff_of_le_one

added theorem Fintype.prod_eq_one_iff_of_one_le

added theorem Fintype.prod_le_one

added theorem Fintype.prod_lt_one

added theorem Fintype.prod_lt_one_iff_of_le_one

modified theorem Fintype.prod_mono'

modified theorem Fintype.prod_strictMono'

Modified Mathlib/Analysis/Convex/Combination.lean

Modified Mathlib/Data/Nat/Digits.lean

Modified Mathlib/NumberTheory/Divisors.lean

Modified Mathlib/Topology/Algebra/InfiniteSum/Order.lean