CyclicProjectionPolynomial.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Polynomial evaluation commutes with the concrete cyclic quotient map.

def OAI.CirculantHadamard.cyclicProjectionAlgHom line 19
Source documentation
The cyclic quotient also preserves the coefficient algebra structure.
```
def cyclicProjectionAlgHom (h : m ∣ n) : Elem R n →ₐ[R] Elem R m :=
…
```
theorem OAI.CirculantHadamard.cyclicProjectionAlgHom_apply line 23
theorem OAI.CirculantHadamard.cyclicProjection_aeval line 27
Source documentation
Polynomial evaluation at the generator commutes with the cyclic quotient.
```
theorem cyclicProjection_aeval (h : m ∣ n) (F : Polynomial R) :
    cyclicProjection R h (Polynomial.aeval (CyclicPolynomial.generator R n) F) =
      Polynomial.aeval (CyclicPolynomial.generator R m) F := by
…
```
Mentions: OAI.CirculantHadamard.cyclicProjection, OAI.CirculantHadamard.CyclicPolynomial.generator