Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-01 17:04 c09501db

View on Github →

feat(*): assorted finset lemmas (#10566)

Estimated changes

Modified src/algebra/big_operators/order.lean

added theorem finset.one_lt_prod

added theorem finset.prod_lt_one

Modified src/data/finset/basic.lean

added theorem finset.range_sdiff_zero