Commit 2023-01-16 13:32 0bebc04d

View on Github →

feat: port Data.Finset.Fold (#1588)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Finset/Fold.lean

added def Finset.fold

added theorem Finset.fold_congr

added theorem Finset.fold_cons

added theorem Finset.fold_const

added theorem Finset.fold_disjUnion

added theorem Finset.fold_disjUnionᵢ

added theorem Finset.fold_empty

added theorem Finset.fold_hom

added theorem Finset.fold_image

added theorem Finset.fold_image_idem

added theorem Finset.fold_insert

added theorem Finset.fold_insert_idem

added theorem Finset.fold_ite'

added theorem Finset.fold_ite

added theorem Finset.fold_map

added theorem Finset.fold_max_add

added theorem Finset.fold_max_le

added theorem Finset.fold_max_lt

added theorem Finset.fold_min_le

added theorem Finset.fold_min_lt

added theorem Finset.fold_op_distrib

added theorem Finset.fold_op_rel_iff_and

added theorem Finset.fold_op_rel_iff_or

added theorem Finset.fold_singleton

added theorem Finset.fold_sup_bot_singleton

added theorem Finset.fold_union_empty_singleton

added theorem Finset.fold_union_inter

added theorem Finset.le_fold_max

added theorem Finset.le_fold_min

added theorem Finset.lt_fold_max

added theorem Finset.lt_fold_min