OAI/NumberTheory/DirichletL/Hecke/DeletionBounds.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SevenEighths.HeckeDeletionBounds.constant_pow_primeSupport_bound line 10
  2. def OAI.SevenEighths.HeckeDeletionBounds.localBound line 32
  3. theorem OAI.SevenEighths.HeckeDeletionBounds.localBound_pos line 34
  4. theorem OAI.SevenEighths.HeckeDeletionBounds.term_bound line 38
  5. theorem OAI.SevenEighths.HeckeDeletionBounds.factor_bounds line 46
  6. theorem OAI.SevenEighths.HeckeDeletionBounds.factors_bound_pow line 71
  7. theorem OAI.SevenEighths.HeckeDeletionBounds.factors_subpower_bound line 94
  8. def OAI.SevenEighths.HeckeDeletionBounds.radical line 106
  9. theorem OAI.SevenEighths.HeckeDeletionBounds.radical_ne_zero line 109
  10. theorem OAI.SevenEighths.HeckeDeletionBounds.factors_radical line 112
  11. theorem OAI.SevenEighths.HeckeDeletionBounds.factors_radical_subpower_bound line 117
  12. theorem OAI.SevenEighths.HeckeDeletionBounds.factor_bound_any_re line 126
  13. theorem OAI.SevenEighths.HeckeDeletionBounds.factors_bound_any_re line 140
  14. theorem OAI.SevenEighths.HeckeDeletionBounds.primeSet_card line 158
  15. theorem OAI.SevenEighths.HeckeDeletionBounds.factors_any_re_subpower_bound line 166