mathlib
97186fe6 - feat(combinatorics): Hindman's theorem on finite sums (#10029)

Commit

4 years ago

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

Author

dwarn

Parents