OAI/NumberTheory/DirichletL/CenteredExceptionalCount.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SevenEighths.CenteredExceptionalCount.valuation line 11
  2. def OAI.SevenEighths.CenteredExceptionalCount.factorMultiset line 13
  3. theorem OAI.SevenEighths.CenteredExceptionalCount.factorMultiset_subset line 16
  4. theorem OAI.SevenEighths.CenteredExceptionalCount.factorMultiset_count line 23
  5. def OAI.SevenEighths.CenteredExceptionalCount.factorPart line 33
  6. theorem OAI.SevenEighths.CenteredExceptionalCount.factorPart_ne_zero line 35
  7. theorem OAI.SevenEighths.CenteredExceptionalCount.factorPart_valuation line 38
  8. def OAI.SevenEighths.CenteredExceptionalCount.sixthRemainder line 44
  9. def OAI.SevenEighths.CenteredExceptionalCount.sixthQuotient line 46
  10. theorem OAI.SevenEighths.CenteredExceptionalCount.sixthRemainder_ne_zero line 48
  11. theorem OAI.SevenEighths.CenteredExceptionalCount.sixthQuotient_ne_zero line 49
  12. theorem OAI.SevenEighths.CenteredExceptionalCount.sixthRemainder_valuation line 51
  13. theorem OAI.SevenEighths.CenteredExceptionalCount.sixthQuotient_valuation line 55
  14. theorem OAI.SevenEighths.CenteredExceptionalCount.valuation_mul line 59
  15. theorem OAI.SevenEighths.CenteredExceptionalCount.valuation_pow line 63
  16. theorem OAI.SevenEighths.CenteredExceptionalCount.ideal_eq_of_valuation_eq line 67
  17. theorem OAI.SevenEighths.CenteredExceptionalCount.sixth_normal_form line 72
  18. theorem OAI.SevenEighths.CenteredExceptionalCount.sixthRemainder_valuation_lt line 82
  19. theorem OAI.SevenEighths.CenteredExceptionalCount.sixthRemainder_eq_iff line 86
  20. theorem OAI.SevenEighths.CenteredExceptionalCount.sixth_normal_form_unique line 96
  21. theorem OAI.SevenEighths.CenteredExceptionalCount.sixthQuotient_injective_on_remainder line 111
  22. theorem OAI.SevenEighths.CenteredExceptionalCount.sixthRemainder_eq_of_profile line 116
  23. theorem OAI.SevenEighths.CenteredExceptionalCount.forced_fourth_power_dvd line 122
  24. theorem OAI.SevenEighths.CenteredExceptionalCount.norm_pos line 139
  25. theorem OAI.SevenEighths.CenteredExceptionalCount.norm_one_le line 142
  26. theorem OAI.SevenEighths.CenteredExceptionalCount.norm_le_of_dvd line 145
  27. theorem OAI.SevenEighths.CenteredExceptionalCount.forced_fourth_power_norm_le line 151
  28. theorem OAI.SevenEighths.CenteredExceptionalCount.sixth_normal_form_norm line 157
  29. theorem OAI.SevenEighths.CenteredExceptionalCount.sixthRemainder_norm_le line 163
  30. theorem OAI.SevenEighths.CenteredExceptionalCount.sixthQuotient_norm_le line 167
  31. theorem OAI.SevenEighths.CenteredExceptionalCount.empty_of_below_remainder line 181
  32. theorem OAI.SevenEighths.CenteredExceptionalCount.ideal_count_fixed_remainder line 191
  33. theorem OAI.SevenEighths.CenteredExceptionalCount.ideal_count_valuation_profile line 217
  34. theorem OAI.SevenEighths.CenteredExceptionalCount.ideal_count_remainder_family line 225
  35. theorem OAI.SevenEighths.CenteredExceptionalCount.ideal_count_of_remainder_norm_lower line 239
  36. theorem OAI.SevenEighths.CenteredExceptionalCount.element_count_le_six_ideal_count line 248
  37. theorem OAI.SevenEighths.CenteredExceptionalCount.element_count_fixed_remainder line 255
  38. theorem OAI.SevenEighths.CenteredExceptionalCount.element_count_valuation_profile line 273
  39. theorem OAI.SevenEighths.CenteredExceptionalCount.element_count_remainder_family line 281
  40. theorem OAI.SevenEighths.CenteredExceptionalCount.elements_empty_of_below_remainder line 295
  41. theorem OAI.SevenEighths.CenteredExceptionalCount.element_count_power_scale line 306
  42. theorem OAI.SevenEighths.CenteredExceptionalCount.ideal_count_power_scale line 324
  43. theorem OAI.SevenEighths.CenteredExceptionalCount.element_count_forced_fourth_power line 342
  44. theorem OAI.SevenEighths.CenteredExceptionalCount.element_count_forced_fourth_power_weaker line 366
  45. theorem OAI.SevenEighths.CenteredExceptionalCount.valuation_eq_multiplicity line 379
  46. theorem OAI.SevenEighths.CenteredExceptionalCount.sixthRemainder_eq_of_prime_profile line 384
  47. theorem OAI.SevenEighths.CenteredExceptionalCount.element_count_power_scale_family line 397
  48. theorem OAI.SevenEighths.CenteredExceptionalCount.element_count_squareNorm line 419