Commit 2023-03-10 07:31 17e458e2

View on Github →

feat: Port/Combinatorics.Hindman (#2280) port of combinatorics.hindman

Estimated changes

Modified Mathlib.lean

Created Mathlib/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 theorem Ultrafilter.continuous_mul_left

added theorem Ultrafilter.eventually_mul

added def Ultrafilter.hasMul

added def Ultrafilter.semigroup

added structure on