Theorem Hindman.FP.tail

Modification history

2026-08-25 15:52
Mathlib/Combinatorics/Hindman.lean
chore: don't inductively define sets (#42171) …
Deleted Hindman.FP.tailView on Github →
2026-08-11 11:20
Mathlib/Combinatorics/Hindman.lean
chore: fix all instances of `linter.defProp` (#42463) …
Added Hindman.FP.tailView on Github →