1214.lean`

1 declarations, 1 contain sorry, 0 declared as axioms

References:

erdosproblems.com/1214
[CoSc97] Corrales-Rodrigáñez, Capi and Schoof, René, The support problem and its elliptic analogue. J. Number Theory (1997) [Volume 64, Issue 2], 276--290.

Imports (1)

theorem Erdos1214.erdos_1214 sorry line 43 source
depends on sorry what this means
Statement uses: Iff, True, Nat, GE.ge, OfNat.ofNat, Eq, Set, Set.ofPred, And, Nat.Prime, Dvd.dvd, HSub.hSub, HPow.hPow
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
18 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
Open to load the checked before-and-after goal states.