Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-08-18 18:52 26590e97

View on Github →

feat(data/list/min_max): maximum is a fold, bounded prod (#8543) Also provide the same lemmas for multiset.

Estimated changes

Modified src/algebra/big_operators/order.lean

added theorem finset.prod_le_of_forall_le

Modified src/data/list/basic.lean

added theorem list.prod_le_of_forall_le

Modified src/data/list/min_max.lean

added theorem list.le_min_of_le_forall

added theorem list.max_le_of_forall_le

added theorem list.max_nat_le_of_forall_le

added theorem list.maximum_eq_coe_foldr_max_of_ne_nil

added theorem list.maximum_nat_eq_coe_foldr_max_of_ne_nil

added theorem list.minimum_eq_coe_foldr_min_of_ne_nil

Modified src/data/multiset/basic.lean

added theorem multiset.prod_le_of_forall_le

Modified src/data/multiset/fold.lean

added theorem multiset.max_le_of_forall_le

added theorem multiset.max_nat_le_of_forall_le