OAI/NumberTheory/DirichletL/Dictionary/InverseRawInput.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SevenEighths.DetectorDictionaryInverseRawInput.admissible_one line 18
  2. theorem OAI.SevenEighths.DetectorDictionaryInverseRawInput.input_generator_one line 22
  3. theorem OAI.SevenEighths.DetectorDictionaryInverseRawInput.complete_pool_selector line 46
  4. theorem OAI.SevenEighths.DetectorDictionaryInverseRawInput.original_complete_star_input line 70
  5. theorem OAI.SevenEighths.DetectorDictionaryInverseRawInput.original_complete_child_norm line 110