OAI/NumberTheory/DirichletL/Hecke/NormFiberCharacters.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.ShortDraftHeckeBridge.normFiberCoeff_baseChangeWeight_zero line 37
  2. def OAI.ShortDraftHeckeBridge.baseChangeChar line 55
  3. theorem OAI.ShortDraftHeckeBridge.baseChangeChar_ne_one_of_one line 60
  4. theorem OAI.ActualEisensteinCubic.canonical_A5_jone_no_quadratic_model line 74
  5. theorem OAI.ShortDraftHeckeBridge.ideals_isRelPrime_of_norms_coprime line 122
  6. theorem OAI.ShortDraftHeckeBridge.baseChangeWeight_mul_of_coprime_norms line 137
  7. theorem OAI.ShortDraftHeckeBridge.baseChangeChar_apply_of_coprime line 146
  8. theorem OAI.ShortDraftHeckeBridge.chiMinusThree_three line 162
  9. theorem OAI.ShortDraftHeckeBridge.baseChangeChar_three line 166
  10. abbrev OAI.ShortDraftHeckeBridge.K line 176
  11. instance OAI.ShortDraftHeckeBridge.(instance at line 177) line 177
  12. instance OAI.ShortDraftHeckeBridge.(instance at line 179) line 179
  13. theorem OAI.ShortDraftHeckeBridge.orderOf_mod3_eq_one line 181
  14. theorem OAI.ShortDraftHeckeBridge.orderOf_mod3_eq_two line 187
  15. theorem OAI.ShortDraftHeckeBridge.degree_two line 199
  16. theorem OAI.ShortDraftHeckeBridge.gal_card_two line 203
  17. theorem OAI.ShortDraftHeckeBridge.not_dvd_three line 207
  18. theorem OAI.ShortDraftHeckeBridge.split_count_of_mod_one line 214
  19. theorem OAI.ShortDraftHeckeBridge.inert_count_of_mod_two line 229
  20. theorem OAI.ShortDraftHeckeBridge.ramified_count line 244
  21. theorem OAI.ShortDraftHeckeBridge.absNorm_split line 249
  22. theorem OAI.ShortDraftHeckeBridge.absNorm_inert line 264
  23. theorem OAI.ShortDraftHeckeBridge.absNorm_ramified line 279
  24. theorem OAI.ShortDraftHeckeBridge.norm_prime_implies_over line 290
  25. theorem OAI.ShortDraftHeckeBridge.norm_p_fiber_split line 303
  26. theorem OAI.ShortDraftHeckeBridge.norm_p_fiber_inert line 314
  27. theorem OAI.ShortDraftHeckeBridge.norm_three_fiber line 326
  28. theorem OAI.ShortDraftHeckeBridge.norm_p_sq_fiber_inert line 337
  29. theorem OAI.ShortDraftHeckeBridge.norm_p_sq_split_factors line 368
  30. theorem OAI.ShortDraftHeckeBridge.norm_p_sq_fiber_split line 392
  31. theorem OAI.ShortDraftHeckeBridge.norm_nine_fiber_ramified line 409
  32. theorem OAI.ShortDraftHeckeBridge.dirichletTarget_of_ideal_base_change line 450
  33. theorem OAI.ShortDraftHeckeBridge.local_inert_p line 498
  34. theorem OAI.ShortDraftHeckeBridge.local_split_p line 505
  35. theorem OAI.ShortDraftHeckeBridge.local_ramified_three line 529
  36. theorem OAI.ShortDraftHeckeBridge.local_inert_p_sq line 552
  37. theorem OAI.ShortDraftHeckeBridge.local_ramified_nine line 580
  38. theorem OAI.ShortDraftHeckeBridge.baseChangeWeight_prime_sq_zero line 608
  39. theorem OAI.ShortDraftHeckeBridge.local_split_p_sq line 618
  40. theorem OAI.ShortDraftHeckeBridge.local_one line 685