OAI/NumberTheory/Ostmann/Arithmetic/ReconstructedWordCoprimality.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The original word coprimalities, with constructed degree and denominator bounds

  1. theorem OAI.Ostmann.HistoryFormula.prime_denominator_unit line 12
  2. theorem OAI.Ostmann.reconstructedWordFormula_frequencies_dvd line 26
  3. theorem OAI.Ostmann.reconstructed_word_coprimality line 35
  4. theorem OAI.Ostmann.zero_reconstructed_word_support line 48
  5. theorem OAI.Ostmann.reconstructed_word_coprimality_removal line 58