OAI/LinearAlgebra/CirculantHadamard/CyclotomicRings.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

The concrete coefficient rings for the prime comparisons

The chosen roots and all coefficient rings live in ℂ. The away ring is proved to be generated by one actual primitive root of order prime to the omitted prime. No equality of root-generated rings is an input hypothesis.

  1. def OAI.CirculantHadamard.CyclotomicRings.rho line 26

    Source documentation

    The fixed primitive root used in the p-direction.

    def rho (p : ℕ) : ℂ := Complex.exp (2 * Real.pi * Complex.I / p)
  2. theorem OAI.CirculantHadamard.CyclotomicRings.rho_isPrimitiveRoot line 28
  3. theorem OAI.CirculantHadamard.CyclotomicRings.rho_zero line 31
  4. theorem OAI.CirculantHadamard.CyclotomicRings.rho_pow line 33
  5. theorem OAI.CirculantHadamard.CyclotomicRings.I_isPrimitiveRoot line 36
  6. theorem OAI.CirculantHadamard.CyclotomicRings.star_eq_pow_pred_of_pow_eq_one line 43

    Source documentation

    Conjugation of a complex root is an explicit nonnegative power.

    theorem star_eq_pow_pred_of_pow_eq_one {z : ℂ} {n : ℕ}
    (hn : n ≠ 0) (hz : z ^ n = 1) : star z = z ^ (n - 1) := by
…
  7. theorem OAI.CirculantHadamard.CyclotomicRings.star_rho line 57
  8. theorem OAI.CirculantHadamard.CyclotomicRings.rho_mul_star line 60
  9. def OAI.CirculantHadamard.CyclotomicRings.GaussianRing line 66
  10. def OAI.CirculantHadamard.CyclotomicRings.gaussianI line 68
  11. theorem OAI.CirculantHadamard.CyclotomicRings.coe_gaussianI line 70
  12. theorem OAI.CirculantHadamard.CyclotomicRings.gaussianI_sq line 72
  13. def OAI.CirculantHadamard.CyclotomicRings.rootRing line 76

    Source documentation

    A finite list of prime directions, keeping i in the coefficient ring.

    def rootRing (s : Finset ℕ) : Subalgebra ℤ ℂ :=
…
  14. abbrev OAI.CirculantHadamard.CyclotomicRings.B line 80

    Source documentation

    The literal global ring in the alternating products.

    abbrev B (u : ℕ) : Subalgebra ℤ ℂ := rootRing u.primeFactors

    Mentions: OAI.CirculantHadamard.CyclotomicRings.rootRing

  15. abbrev OAI.CirculantHadamard.CyclotomicRings.awayRing line 83

    Source documentation

    The literal coefficient ring with the p-direction omitted.

    abbrev awayRing (u p : ℕ) : Subalgebra ℤ ℂ := rootRing (u.primeFactors.erase p)

    Mentions: OAI.CirculantHadamard.CyclotomicRings.rootRing

  16. theorem OAI.CirculantHadamard.CyclotomicRings.I_mem_rootRing line 85
  17. theorem OAI.CirculantHadamard.CyclotomicRings.rho_mem_rootRing line 88
  18. theorem OAI.CirculantHadamard.CyclotomicRings.I_mem_B line 91
  19. theorem OAI.CirculantHadamard.CyclotomicRings.rho_mem_B line 93
  20. theorem OAI.CirculantHadamard.CyclotomicRings.I_mem_awayRing line 96
  21. theorem OAI.CirculantHadamard.CyclotomicRings.rho_mem_awayRing line 98
  22. theorem OAI.CirculantHadamard.CyclotomicRings.rootRing_mono line 102
  23. theorem OAI.CirculantHadamard.CyclotomicRings.GaussianRing_le_rootRing line 106
  24. theorem OAI.CirculantHadamard.CyclotomicRings.awayRing_le_B line 109
  25. def OAI.CirculantHadamard.CyclotomicRings.awayInclusion line 112
  26. def OAI.CirculantHadamard.CyclotomicRings.gaussianToB line 115
  27. def OAI.CirculantHadamard.CyclotomicRings.gaussianToAway line 118
  28. theorem OAI.CirculantHadamard.CyclotomicRings.coe_awayInclusion line 121
  29. theorem OAI.CirculantHadamard.CyclotomicRings.coe_gaussianToB line 126
  30. theorem OAI.CirculantHadamard.CyclotomicRings.coe_gaussianToAway line 131
  31. theorem OAI.CirculantHadamard.CyclotomicRings.gaussian_mem line 136
  32. theorem OAI.CirculantHadamard.CyclotomicRings.star_mem_adjoin line 141
  33. theorem OAI.CirculantHadamard.CyclotomicRings.star_mem_GaussianRing line 153
  34. theorem OAI.CirculantHadamard.CyclotomicRings.star_mem_rootRing line 159
  35. instance OAI.CirculantHadamard.CyclotomicRings.GaussianRingStarRing line 170
  36. instance OAI.CirculantHadamard.CyclotomicRings.rootRingStarRing line 176
  37. theorem OAI.CirculantHadamard.CyclotomicRings.coe_star_GaussianRing line 182
  38. theorem OAI.CirculantHadamard.CyclotomicRings.coe_star_rootRing line 185
  39. theorem OAI.CirculantHadamard.CyclotomicRings.gaussianToB_star line 188
  40. theorem OAI.CirculantHadamard.CyclotomicRings.gaussianToAway_star line 196
  41. theorem OAI.CirculantHadamard.CyclotomicRings.rho_finite_order line 204
  42. theorem OAI.CirculantHadamard.CyclotomicRings.map_star_of_pow_eq_one line 209
  43. theorem OAI.CirculantHadamard.CyclotomicRings.map_star_adjoin line 220
  44. theorem OAI.CirculantHadamard.CyclotomicRings.map_star_rootRing line 245

    Source documentation

    Every complex-valued ring map respects the actual conjugation.

    theorem map_star_rootRing (s : Finset ℕ) (σ : rootRing s →+* ℂ) (x : rootRing s) :
    σ (star x) = star (σ x) := by
…

    Mentions: OAI.CirculantHadamard.CyclotomicRings.rootRing

  45. theorem OAI.CirculantHadamard.CyclotomicRings.map_star_B line 254
  46. theorem OAI.CirculantHadamard.CyclotomicRings.map_star_awayRing line 257
  47. theorem OAI.CirculantHadamard.CyclotomicRings.map_star_GaussianRing line 260
  48. theorem OAI.CirculantHadamard.CyclotomicRings.integral_of_finite_order line 267
  49. instance OAI.CirculantHadamard.CyclotomicRings.rootRing_finite line 274
  50. instance OAI.CirculantHadamard.CyclotomicRings.GaussianRing_finite line 282
  51. theorem OAI.CirculantHadamard.CyclotomicRings.primitive_mul line 286
  52. theorem OAI.CirculantHadamard.CyclotomicRings.prime_roots_prod_primitive line 295
  53. def OAI.CirculantHadamard.CyclotomicRings.etaOf line 316

    Source documentation

    The single generator of a finite prime-root ring.

    def etaOf (s : Finset ℕ) : ℂ := Complex.I * ∏ q ∈ s, rho q

    Mentions: OAI.CirculantHadamard.CyclotomicRings.rho

  54. def OAI.CirculantHadamard.CyclotomicRings.orderOfSet line 318
  55. theorem OAI.CirculantHadamard.CyclotomicRings.etaOf_isPrimitiveRoot line 320
  56. theorem OAI.CirculantHadamard.CyclotomicRings.orderOfSet_pos line 328
  57. theorem OAI.CirculantHadamard.CyclotomicRings.rootRing_eq_singleton line 332
  58. def OAI.CirculantHadamard.CyclotomicRings.eta line 359
  59. def OAI.CirculantHadamard.CyclotomicRings.awayOrder line 361
  60. theorem OAI.CirculantHadamard.CyclotomicRings.eta_isPrimitiveRoot line 363
  61. theorem OAI.CirculantHadamard.CyclotomicRings.awayOrder_pos line 371
  62. theorem OAI.CirculantHadamard.CyclotomicRings.awayRing_eq_singleton line 374
  63. theorem OAI.CirculantHadamard.CyclotomicRings.prime_not_dvd_awayOrder line 382
  64. theorem OAI.CirculantHadamard.CyclotomicRings.B_eq_adjoin_away line 397