PrimeComponents.lean`

36 declarations, 0 contain sorry, 0 declared as axioms

Actual primary components of the cyclic group of order u²

The prime set is the literal finite set of prime factors of u. The exponent of each component is (u ^ 2).factorization p, hence twice the exponent in u. Factorization and coprimality supply the hypotheses of the finite Chinese remainder theorem. Its coordinates are the canonical reduction maps.

The generator of each primary component is the inverse image of its unit coordinate vector. Its additive order is proved to be the full prime power, and the complementary integer factor of u² is proved prime to p.

def OAI.CirculantHadamard.PrimeComponents.primes line 27
abbrev OAI.CirculantHadamard.PrimeComponents.PrimeIndex line 29
def OAI.CirculantHadamard.PrimeComponents.exponent line 31
def OAI.CirculantHadamard.PrimeComponents.order line 33
abbrev OAI.CirculantHadamard.PrimeComponents.Component line 35
abbrev OAI.CirculantHadamard.PrimeComponents.PrimaryProduct line 37
theorem OAI.CirculantHadamard.PrimeComponents.mem_primes line 39
theorem OAI.CirculantHadamard.PrimeComponents.prime_of_mem line 42
theorem OAI.CirculantHadamard.PrimeComponents.dvd_of_mem line 45
theorem OAI.CirculantHadamard.PrimeComponents.primes_nonempty line 48
theorem OAI.CirculantHadamard.PrimeComponents.prime_ne_two_of_odd line 51
theorem OAI.CirculantHadamard.PrimeComponents.odd_of_mem line 56
theorem OAI.CirculantHadamard.PrimeComponents.exponent_eq_two_mul line 60
Source documentation
The scalar exponent in local comparison is the exponent in u².
```
theorem exponent_eq_two_mul (u p : ℕ) : exponent u p = 2 * u.factorization p := by
…
```
Mentions: OAI.CirculantHadamard.PrimeComponents.exponent
theorem OAI.CirculantHadamard.PrimeComponents.exponent_pos line 63
theorem OAI.CirculantHadamard.PrimeComponents.order_pos line 68
instance OAI.CirculantHadamard.PrimeComponents.componentOrder_neZero line 71
theorem OAI.CirculantHadamard.PrimeComponents.prime_dvd_order line 74
theorem OAI.CirculantHadamard.PrimeComponents.order_dvd_square line 77
theorem OAI.CirculantHadamard.PrimeComponents.next_power_not_dvd line 81
Source documentation
This is the full primary factor: the next power does not divide u².
```
theorem next_power_not_dvd {u p : ℕ} (hu : 0 < u) (hp : p ∈ primes u) :
    ¬p ^ (exponent u p + 1) ∣ u ^ 2 :=
…
```
Mentions: OAI.CirculantHadamard.PrimeComponents.primes, OAI.CirculantHadamard.PrimeComponents.exponent
def OAI.CirculantHadamard.PrimeComponents.cofactor line 85
theorem OAI.CirculantHadamard.PrimeComponents.order_mul_cofactor line 87
theorem OAI.CirculantHadamard.PrimeComponents.cofactor_not_dvd line 90
theorem OAI.CirculantHadamard.PrimeComponents.cofactor_coprime line 94
theorem OAI.CirculantHadamard.PrimeComponents.prod_order_finset line 98
theorem OAI.CirculantHadamard.PrimeComponents.prod_order line 104
theorem OAI.CirculantHadamard.PrimeComponents.pairwise_coprime line 110
def OAI.CirculantHadamard.PrimeComponents.crtRing line 117
Source documentation
The actual finite Chinese remainder equivalence, with no chosen-map premise.
```
def crtRing (u : ℕ) (hu : 0 < u) : ZMod (u ^ 2) ≃+* PrimaryProduct u :=
…
```
Mentions: OAI.CirculantHadamard.PrimeComponents.PrimaryProduct
def OAI.CirculantHadamard.PrimeComponents.crt line 121
theorem OAI.CirculantHadamard.PrimeComponents.crt_intCast line 124
theorem OAI.CirculantHadamard.PrimeComponents.crt_natCast line 129
theorem OAI.CirculantHadamard.PrimeComponents.crt_apply line 135
Source documentation
Every CRT coordinate is literal reduction from ZMod(u²) to the full p-power.
```
theorem crt_apply (u : ℕ) (hu : 0 < u) (x : ZMod (u ^ 2)) (p : PrimeIndex u) :
    crt u hu x p = (ZMod.cast x : Component u p) := by
…
```
Mentions: OAI.CirculantHadamard.PrimeComponents.PrimeIndex, OAI.CirculantHadamard.PrimeComponents.crt, OAI.CirculantHadamard.PrimeComponents.Component
def OAI.CirculantHadamard.PrimeComponents.primaryGenerator line 140
theorem OAI.CirculantHadamard.PrimeComponents.crt_primaryGenerator line 143
theorem OAI.CirculantHadamard.PrimeComponents.crt_primaryGenerator_same line 147
theorem OAI.CirculantHadamard.PrimeComponents.crt_primaryGenerator_ne line 151
theorem OAI.CirculantHadamard.PrimeComponents.primaryGenerator_addOrderOf line 157
Source documentation
The chosen primary generator has exactly the full primary order.
```
theorem primaryGenerator_addOrderOf (u : ℕ) (hu : 0 < u) (p : PrimeIndex u) :
    addOrderOf (primaryGenerator u hu p) = order u p.val := by
…
```
Mentions: OAI.CirculantHadamard.PrimeComponents.PrimeIndex, OAI.CirculantHadamard.PrimeComponents.primaryGenerator, OAI.CirculantHadamard.PrimeComponents.order