FormalConjectures/ErdosProblems/397.lean

GitHub source file

1 declarations, 1 contain sorry, 0 declared as axioms

Erdős Problem 397

References:

Imports (1)
  1. theorem Erdos397.erdos_397 sorry line 54 source

    depends on sorry what this means

    Statement uses: Iff, False, Set.Finite, Prod, Finset, Nat, Set.ofPred, Erdos397.erdos_397.match_1, And, Disjoint, Eq, Finset.prod, Nat.centralBinom

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

    7 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

    Open to load the checked before-and-after goal states.