CyclicEvaluationProjection.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Evaluation at a root of smaller order factors through the cyclic quotient.

theorem OAI.CirculantHadamard.evaluateAt_cyclicProjection line 21
Source documentation
The actual root evaluation is unchanged after reducing the cyclic index. Both root equations are stated explicitly to match the two evaluation maps.
```
theorem evaluateAt_cyclicProjection (h : m ∣ n)
    (x : S) (hm : x ^ m = 1) (hn : x ^ n = 1) (F : Elem R n) :
    evaluateAt m x hm (cyclicProjection R h F) = evaluateAt n x hn F := by
…
```
Mentions: OAI.CirculantHadamard.cyclicProjection