OAI/NumberTheory/Ostmann/PaperMain.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Main statements of The additive indecomposability of the primes

  1. theorem OAI.OstmannPaper.inverse_goldbach line 12

    Source documentation

    Theorem 1.1, including every finite modification of the primes.

    theorem inverse_goldbach (A B : Set ℕ) (hA : A.Nontrivial) (hB : B.Nontrivial) :
    (Ostmann.sumset A B ∆ Ostmann.primes).Infinite :=
…

    Mentions: OAI.Ostmann.sumset, OAI.Ostmann.primes

  2. theorem OAI.OstmannPaper.two_infinite_summands line 17

    Source documentation

    Theorem 2.3, the two-infinite-summand formulation.

    theorem two_infinite_summands (A B : Set ℕ) (hA : A.Infinite) (hB : B.Infinite) :
    ¬ (Ostmann.sumset A B ∆ Ostmann.primes).Finite := by
…

    Mentions: OAI.Ostmann.sumset, OAI.Ostmann.primes