OAI/NumberTheory/DirichletL/ConductorBounds.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SevenEighths.FiniteConductor.quotient_card_le_of_le line 18
  2. theorem OAI.SevenEighths.FiniteConductor.quotient_inf_card_le_mul line 22
  3. def OAI.SevenEighths.FiniteConductor.quotientComapEquiv line 35
  4. theorem OAI.SevenEighths.FiniteConductor.quotientComapEquiv_mk line 41
  5. theorem OAI.SevenEighths.FiniteConductor.quotient_comap_card line 45
  6. theorem OAI.SevenEighths.FiniteConductor.primitive_of_maximal_descent line 55
  7. theorem OAI.SevenEighths.FiniteConductor.exists_primitive_quotient_above line 84
  8. theorem OAI.SevenEighths.FiniteConductor.exists_primitive_quotient_above_with_bound_and_mask line 95
  9. theorem OAI.SevenEighths.FiniteConductor.FactorsThroughIdeal.mul line 107
  10. theorem OAI.SevenEighths.FiniteConductor.exists_primitive_product_quotient_with_bound_and_mask line 114
  11. theorem OAI.SevenEighths.FiniteConductor.absNorm_le_of_le line 133
  12. theorem OAI.SevenEighths.FiniteConductor.absNorm_inf_le_mul line 138
  13. theorem OAI.SevenEighths.FiniteConductor.absNorm_comap_eq_quotient_card line 143
  14. theorem OAI.SevenEighths.FiniteConductor.absNorm_comap_le line 147
  15. theorem OAI.SevenEighths.FiniteConductor.exists_primitive_residue_quotient_above_with_norm_and_mask line 155
  16. theorem OAI.SevenEighths.FiniteConductor.exists_primitive_residue_product_with_norm_and_mask line 169