CyclicPolynomial.lean`

23 declarations, 0 contain sorry, 0 declared as axioms

The polynomial presentation of the actual cyclic group algebra

For a commutative coefficient ring and a positive integer n, the cyclic group algebra is the quotient of R[X] by X ^ n - 1. The two maps are defined by their universal properties, and both inverse identities are proved explicitly. No domain property of the finite group algebra is used.

def OAI.CirculantHadamard.CyclicPolynomial.relation line 27
Source documentation
The defining polynomial of the cyclic group algebra.
```
def relation : R[X] := X ^ n - 1
```
def OAI.CirculantHadamard.CyclicPolynomial.generator line 30
Source documentation
The basis element at the distinguished generator of the cyclic group.
```
def generator : AddMonoidAlgebra R (ZMod n) := AddMonoidAlgebra.single 1 1
```
theorem OAI.CirculantHadamard.CyclicPolynomial.generator_pow line 32
theorem OAI.CirculantHadamard.CyclicPolynomial.root_pow line 36
def OAI.CirculantHadamard.CyclicPolynomial.powerCharacter line 45
Source documentation
A genuine cyclic character associated to an element whose nth power is one.
```
def powerCharacter {A : Type uA} [Monoid A] [NeZero n]
    (x : A) (hx : x ^ n = 1) : Multiplicative (ZMod n) →* A where
…
```
theorem OAI.CirculantHadamard.CyclicPolynomial.powerCharacter_apply line 57
theorem OAI.CirculantHadamard.CyclicPolynomial.powerCharacter_generator line 62
def OAI.CirculantHadamard.CyclicPolynomial.toPolynomial line 71
Source documentation
Send the cyclic basis element at i to the i.valth power of the root.
```
def toPolynomial [NeZero n] :
    AddMonoidAlgebra R (ZMod n) →ₐ[R] AdjoinRoot (relation R n) :=
…
```
Mentions: OAI.CirculantHadamard.CyclicPolynomial.relation
theorem OAI.CirculantHadamard.CyclicPolynomial.toPolynomial_single line 77
theorem OAI.CirculantHadamard.CyclicPolynomial.toPolynomial_generator line 84
theorem OAI.CirculantHadamard.CyclicPolynomial.generator_isRoot line 89
def OAI.CirculantHadamard.CyclicPolynomial.fromPolynomial line 93
Source documentation
Evaluate the polynomial quotient at the actual cyclic group-ring generator.
```
def fromPolynomial :
    AdjoinRoot (relation R n) →ₐ[R] AddMonoidAlgebra R (ZMod n) :=
…
```
Mentions: OAI.CirculantHadamard.CyclicPolynomial.relation
theorem OAI.CirculantHadamard.CyclicPolynomial.fromPolynomial_root line 100
theorem OAI.CirculantHadamard.CyclicPolynomial.fromPolynomial_mk line 107
theorem OAI.CirculantHadamard.CyclicPolynomial.generator_pow_val line 114
theorem OAI.CirculantHadamard.CyclicPolynomial.toPolynomial_comp_fromPolynomial line 118
theorem OAI.CirculantHadamard.CyclicPolynomial.fromPolynomial_comp_toPolynomial line 124
def OAI.CirculantHadamard.CyclicPolynomial.cyclicEquiv line 133
Source documentation
The actual cyclic group algebra is the polynomial quotient by X ^ n - 1.
```
def cyclicEquiv [NeZero n] :
    AddMonoidAlgebra R (ZMod n) ≃ₐ[R] AdjoinRoot (relation R n) :=
…
```
Mentions: OAI.CirculantHadamard.CyclicPolynomial.relation
theorem OAI.CirculantHadamard.CyclicPolynomial.cyclicEquiv_single line 139
theorem OAI.CirculantHadamard.CyclicPolynomial.cyclicEquiv_generator line 146
theorem OAI.CirculantHadamard.CyclicPolynomial.cyclicEquiv_symm_root line 151
theorem OAI.CirculantHadamard.CyclicPolynomial.cyclicEquiv_symm_mk line 156
theorem OAI.CirculantHadamard.CyclicPolynomial.cyclicEquiv_aeval line 162