Theorem Hindman.FP.cons

Modification history

2026-08-25 15:52

Mathlib/Combinatorics/Hindman.lean

chore: don't inductively define sets (#42171) …

Deleted Hindman.FP.cons View on Github →

2026-08-11 11:20

Mathlib/Combinatorics/Hindman.lean

chore: fix all instances of `linter.defProp` (#42463) …

Added Hindman.FP.cons View on Github →