171.lean`

1 declarations, 1 contain sorry, 0 declared as axioms

References:

erdosproblems.com/171
[ErGr79] Erdős, P. and Graham, R., Old and new problems and results in combinatorial number theory: van der Waerden's theorem and related topics. Enseign. Math. (1979), 325-344.
[ErGr80] Erdős, P. and Graham, R., Old and new problems and results in combinatorial number theory. Monographies de L'Enseignement Mathematique (1980).
[FuKa91] Furstenberg, H. and Katznelson, Y., A density version of the Hales-Jewett Theorem. Journal d'Analyse Mathématique (1991), 64-119.
[Po12] Polymath, D. H. J., A new proof of the density Hales–Jewett theorem. Ann. Math. (2012), 1283-1327.

Imports (1)

theorem Erdos171.erdos_171 sorry line 56 source
depends on sorry what this means
Statement uses: Iff, True, Real, LT.lt, OfNat.ofNat, Nat, LE.le, Filter.Eventually, Finset, Fin, HMul.hMul, HPow.hPow, Finset.card, Exists, Combinatorics.Line, Membership.mem, Filter.atTop
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
36 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
Open to load the checked before-and-after goal states.