OAI/NumberTheory/DirichletL/CenteredExceptionalProfile.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SevenEighths.CenteredExceptionalProfile.split_at_prime line 17
  2. theorem OAI.SevenEighths.CenteredExceptionalProfile.exists_unit_probe line 42
  3. theorem OAI.SevenEighths.CenteredExceptionalProfile.valuation_mod_six_of_unit_agreement line 65
  4. def OAI.SevenEighths.CenteredExceptionalProfile.InducedBy line 96
  5. theorem OAI.SevenEighths.CenteredExceptionalProfile.exists_primitive_inducedBy line 100
  6. theorem OAI.SevenEighths.CenteredExceptionalProfile.elementCoeff_eq_of_inducedBy line 106
  7. theorem OAI.SevenEighths.CenteredExceptionalProfile.elementCoeff_eq_one_of_inducedBy line 113
  8. theorem OAI.SevenEighths.CenteredExceptionalProfile.local_rows_profile line 125
  9. theorem OAI.SevenEighths.CenteredExceptionalProfile.actual_row_on_fixed_units line 155
  10. theorem OAI.SevenEighths.CenteredExceptionalProfile.actual_rows_good_profile line 176
  11. theorem OAI.SevenEighths.CenteredExceptionalProfile.valuation_span_eq_zero_of_not_mem line 200
  12. theorem OAI.SevenEighths.CenteredExceptionalProfile.valuation_supported_numerator line 208
  13. theorem OAI.SevenEighths.CenteredExceptionalProfile.valuation_mod_six_cancel_frozen line 226
  14. theorem OAI.SevenEighths.CenteredExceptionalProfile.actual_rows_profile line 233
  15. theorem OAI.SevenEighths.CenteredExceptionalProfile.local_row_valuation_zero line 260
  16. theorem OAI.SevenEighths.CenteredExceptionalProfile.actual_row_numerator_valuation_zero line 285
  17. theorem OAI.SevenEighths.CenteredExceptionalProfile.actual_row_forced_residue_four line 302
  18. theorem OAI.SevenEighths.CenteredExceptionalProfile.actual_forced_fourth_power line 319
  19. def OAI.SevenEighths.CenteredExceptionalProfile.FixedInducingRow line 338
  20. theorem OAI.SevenEighths.CenteredExceptionalProfile.fixed_inducing_rows_profile line 343
  21. theorem OAI.SevenEighths.CenteredExceptionalProfile.fixed_inducing_rows_same_remainder line 360
  22. theorem OAI.SevenEighths.CenteredExceptionalProfile.fixed_inducing_remainder_card line 380
  23. theorem OAI.SevenEighths.CenteredExceptionalProfile.fixed_inducing_row_count line 405
  24. theorem OAI.SevenEighths.CenteredExceptionalProfile.outside_fixed_support line 446
  25. theorem OAI.SevenEighths.CenteredExceptionalProfile.fixed_support_exceptional_count line 477
  26. theorem OAI.SevenEighths.CenteredExceptionalProfile.fixed_support_exceptional_count_weaker line 494
  27. theorem OAI.SevenEighths.CenteredExceptionalProfile.fixed_inducing_rows_empty line 512