OAI/NumberTheory/Ostmann/Corollaries.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Prime-sumset indecomposability and its finite-modification and composite-sum consequences.

  1. theorem OAI.NumberTheory.Ostmann.main line 11
  2. theorem OAI.NumberTheory.Ostmann.finite_modification_indecomposable line 15
  3. theorem OAI.NumberTheory.Ostmann.infinite_summands line 22
  4. theorem OAI.NumberTheory.Ostmann.infinitely_many_nonprime_sums line 26
  5. theorem OAI.NumberTheory.Ostmann.infinitely_many_composite_sums line 41