Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-11-23 16:49 97186fe6

View on Github →

feat(combinatorics): Hindman's theorem on finite sums (#10029) A short proof of Hindman's theorem using idempotent ultrafilters.

Estimated changes

Created src/combinatorics/hindman.lean

added theorem hindman.FP.finset_prod

added theorem hindman.FP.mul

added theorem hindman.FP.mul_two

added theorem hindman.FP.singleton

added inductive hindman.FP

added theorem hindman.FP_drop_subset_FP

added theorem hindman.FP_partition_regular

added inductive hindman.FS

added theorem hindman.exists_FP_of_finite_cover

added theorem hindman.exists_FP_of_large

added theorem hindman.exists_idempotent_ultrafilter_le_FP

added structure on

added theorem ultrafilter.continuous_mul_left

added theorem ultrafilter.eventually_mul

added def ultrafilter.has_mul

added def ultrafilter.semigroup

Modified src/data/stream/basic.lean

added theorem stream.head_drop

Modified src/order/filter/ultrafilter.lean

Created src/topology/algebra/semigroup.lean

added theorem exists_idempotent_in_compact_subsemigroup

added theorem exists_idempotent_of_compact_t2_of_continuous_mul_left