Formal target: Corpus.WikipediaCongruentNumber.Tunnell_odd_converse

Tunnell's theorem (sufficient condition assuming BSD) for odd squarefree congruent numbers.

Exact formal statement

∀ (n : Nat),
  Squarefree.{0} n →
    Odd.{0} n →
      Eq.{1} (HMul.hMul.{0, 0, 0} 2 (Set.ncard.{0} (Corpus.WikipediaCongruentNumber.A n)))
          (Set.ncard.{0} (Corpus.WikipediaCongruentNumber.B n)) →
        Corpus.WikipediaCongruentNumber.congruentNumber n

This target is a formal statement, not a proof of the problem.

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record