OAI/NumberTheory/Ostmann/Arithmetic/HistorySupportReductionBasic.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Ostmann.Arithmetic.HistorySupportReduction.RootData line 12
  2. def OAI.Ostmann.Arithmetic.HistorySupportReduction.LargePrimes line 16
  3. def OAI.Ostmann.Arithmetic.HistorySupportReduction.LocalTests line 22
  4. def OAI.Ostmann.Arithmetic.HistorySupportReduction.Reduced line 30
  5. theorem OAI.Ostmann.Arithmetic.HistorySupportReduction.root_frequency_mem line 39
  6. theorem OAI.Ostmann.Arithmetic.HistorySupportReduction.rootData_of_supported line 42
  7. theorem OAI.Ostmann.Arithmetic.HistorySupportReduction.largePrimes_root line 47
  8. theorem OAI.Ostmann.Arithmetic.HistorySupportReduction.root_frequency_small_units line 53
  9. theorem OAI.Ostmann.Arithmetic.HistorySupportReduction.inherited_frequency_unit line 62
  10. theorem OAI.Ostmann.Arithmetic.HistorySupportReduction.child_list_coprime_of_state line 79