FormalConjectures/ErdosProblems/260.lean

GitHub source file

1 declarations, 1 contain sorry, 0 declared as axioms

Erdős Problem 260

References:

Imports (1)
Imported by 1 file
  1. theorem Erdos260.erdos_260 sorry line 44 source

    depends on sorry what this means

    Statement uses: Iff, True, Nat, Int, Real, StrictMono, Filter.Tendsto, HDiv.hDiv, Filter.atTop, HasSum, HPow.hPow, OfNat.ofNat, SummationFilter.unconditional, Irrational

    Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

    52 instances, coercions and auxiliary constants left out.