OAI/NumberTheory/DirichletL/Reciprocity/RamifiedSymbol.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CubicRamified.cubicExp line 78
  2. lemma OAI.CubicRamified.cubicExp_eq_of_dvd_sub line 80
  3. lemma OAI.CubicRamified.cubicExp_add line 85
  4. lemma OAI.CubicRamified.cubicExp_zero line 91
  5. def OAI.CubicRamified.linearRay line 93
  6. lemma OAI.CubicRamified.linearRay_primaryCoord line 97
  7. lemma OAI.CubicRamified.exists_primaryCoord line 103
  8. lemma OAI.CubicRamified.primaryCoord_mul line 117
  9. lemma OAI.CubicRamified.linearRay_one line 123
  10. lemma OAI.CubicRamified.linearRay_mul line 128
  11. theorem OAI.CubicRamified.symbol_eq_linearRay_of_prime line 140
  12. theorem OAI.CubicRamified.symbol_lambda_eq_linearRay line 158
  13. theorem OAI.CubicRamified.symbol_omega_eq_linearRay line 172
  14. theorem OAI.CubicRamified.cubicValue_traceLambda_primary line 186
  15. theorem OAI.CubicRamified.symbol_traceLambda_eq_linearRay line 198
  16. theorem OAI.CubicRamified.linearRay_congr_mod_nine line 212
  17. theorem OAI.CubicRamified.symbol_lambda_congr_mod_nine line 236
  18. theorem OAI.CubicRamified.symbol_traceLambda_congr_mod_nine line 242
  19. theorem OAI.CubicJacobiGlobal.primary_ne_zero line 253
  20. theorem OAI.CubicJacobiGlobal.symbol_one_numerator line 257
  21. theorem OAI.CubicJacobiGlobal.symbol_mul_numerator line 262
  22. theorem OAI.CubicJacobiGlobal.symbol_pow_numerator line 268
  23. theorem OAI.CubicJacobiGlobal.symbol_neg_one line 274
  24. theorem OAI.CubicJacobiGlobal.symbol_neg_numerator line 284
  25. theorem OAI.CubicJacobiGlobal.symbol_isUnit_ne_zero line 288
  26. theorem OAI.CubicJacobiGlobal.symbol_unit_congr_mod_nine line 298
  27. theorem OAI.CubicJacobiGlobal.associated_congr_denominator line 324
  28. theorem OAI.CubicJacobiGlobal.ramified_prime line 337
  29. theorem OAI.CubicJacobiGlobal.symbol_prime_denominator_congr line 341
  30. theorem OAI.CubicJacobiGlobal.symbol_denominator_congr line 358
  31. def OAI.PrimaryIdealUnitReindex.unitCoordinates line 376
  32. theorem OAI.PrimaryIdealUnitReindex.q_eq_one_iff_unitCoordinates line 379
  33. theorem OAI.PrimaryIdealUnitReindex.unit_coordinate_mem line 393
  34. def OAI.PrimaryIdealUnitReindex.unitCoordinateMap line 401
  35. theorem OAI.PrimaryIdealUnitReindex.unitCoordinateMap_bijective line 404
  36. def OAI.PrimaryIdealUnitReindex.unitCoordinateEquiv line 421
  37. theorem OAI.PrimaryIdealUnitReindex.card_units_eq_six line 424
  38. theorem OAI.QuadraticUnitInvariance.rowCoprimeMask_unit_mul line 436
  39. theorem OAI.QuadraticUnitInvariance.rowCoprimeMask_norm_le_one line 441
  40. theorem OAI.QuadraticUnitInvariance.masked_two_rows_radial_summable line 446
  41. theorem OAI.QuadraticUnitInvariance.quadratic_pair_lattice_eq_primary_ideal_sum line 469
  42. theorem OAI.GaussGeneratorTransport.canonical_masked_radial_poisson_product line 512
  43. theorem OAI.QuadraticUnitInvariance.odd_of_quadraticRayValue_norm_eq_one line 560
  44. theorem OAI.QuadraticUnitInvariance.quadraticBlock_union_eq_one_of_same_ray line 567
  45. theorem OAI.QuadraticUnitInvariance.same_ray_quadratic_pair_poisson line 582
  46. theorem OAI.EisensteinSchwartzPoisson.paperRadialFourier_nonzero_lattice_decay line 629
  47. theorem OAI.EisensteinSchwartzPoisson.paperRadialFourier_nonzero_sum_decay line 653
  48. theorem OAI.EisensteinSchwartzPoisson.principal_tail_scalar line 674
  49. theorem OAI.EisensteinSchwartzPoisson.maskedPrincipalRemainder_large_scale line 689