OAI/NumberTheory/DirichletL/Inversion/InitialExcludedPeriod.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SevenEighths.InverseInitialExcludedPeriod.deletedPeriod line 15
  2. theorem OAI.SevenEighths.InverseInitialExcludedPeriod.deletedPeriod_ne_zero line 17
  3. theorem OAI.SevenEighths.InverseInitialExcludedPeriod.fixed_bad_divides_reflection line 21
  4. theorem OAI.SevenEighths.InverseInitialExcludedPeriod.excluded_mem_iff line 41
  5. theorem OAI.SevenEighths.InverseInitialExcludedPeriod.excluded_product_divides_reflection line 52
  6. theorem OAI.SevenEighths.InverseInitialExcludedPeriod.deleted_reflection_ideal line 62
  7. theorem OAI.SevenEighths.InverseInitialExcludedPeriod.deleted_excluded_eq line 71
  8. theorem OAI.SevenEighths.InverseInitialExcludedPeriod.deleted_period_ideal line 82
  9. theorem OAI.SevenEighths.InverseInitialExcludedPeriod.deleted_period_le_modulus line 91
  10. theorem OAI.SevenEighths.InverseInitialExcludedPeriod.deleted_element_period line 99
  11. theorem OAI.SevenEighths.InverseInitialExcludedPeriod.deleted_base_gates line 108