CoefficientEvaluation.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Changing coefficients in an actual cyclic group ring

The group coordinate is retained unchanged. Character evaluation and augmentation commute with this coefficient map, including localization of the away ring.

def OAI.CirculantHadamard.CyclicRing.coefficientMap line 23
Source documentation
Map coefficients and retain the same cyclic basis.
```
def coefficientMap (φ : R →+* S) (n : ℕ) : Elem R n →+* Elem S n :=
…
```
Mentions: OAI.CirculantHadamard.CyclicRing.Elem
theorem OAI.CirculantHadamard.CyclicRing.coefficientMap_single line 26
theorem OAI.CirculantHadamard.CyclicRing.coefficientMap_scalar line 32
theorem OAI.CirculantHadamard.CyclicRing.evaluate_coefficientMap_hom line 37
Source documentation
Bundled naturality; no root-of-unity or nonzero-modulus premise is needed.
```
theorem evaluate_coefficientMap_hom (φ : R →+* S) (ψ : S →+* T) (n : ℕ)
    (χ : Multiplicative (ZMod n) →* T) :
    (evaluate ψ χ).comp (coefficientMap φ n) = evaluate (ψ.comp φ) χ := by
…
```
Mentions: OAI.CirculantHadamard.CyclicRing.evaluate, OAI.CirculantHadamard.CyclicRing.coefficientMap
theorem OAI.CirculantHadamard.CyclicRing.evaluate_coefficientMap line 46
theorem OAI.CirculantHadamard.CyclicRing.augmentation_coefficientMap line 51