CyclotomicIntegerEvaluation.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Integer cyclic evaluation and actual cyclotomic conjugation

The coefficient map is the integer cast into the cyclotomic quotient. The character sends the cyclic generator to its adjoined root. The root-inverting automorphism therefore carries evaluation to evaluation of the actual cyclic group-ring involution.

def OAI.CirculantHadamard.integerCyclotomicEvaluation line 28
Source documentation
Integer cyclic group-ring evaluation in the actual cyclotomic quotient.
```
def integerCyclotomicEvaluation :
    CyclicRing.Elem ℤ n →+* AdjoinRoot (cyclotomic n A) :=
…
```
Mentions: OAI.CirculantHadamard.CyclicRing.Elem
theorem OAI.CirculantHadamard.integerCyclotomicEvaluation_apply line 34
theorem OAI.CirculantHadamard.integerCyclotomicEvaluation_scalar line 41

theorem OAI.CirculantHadamard.cyclotomicPowerCharacter_neg line 52

Source documentation

The actual character intertwines negation of its index and the proved cyclotomic conjugation.

theorem cyclotomicPowerCharacter_neg (a : ZMod n) :
    CyclicPolynomial.powerCharacter n (AdjoinRoot.root (cyclotomic n A))
        (RamifiedConjugation.root_pow_order A n) (Multiplicative.ofAdd (-a)) =
      RamifiedConjugation.cyclotomicConjugation A n hn
        (CyclicPolynomial.powerCharacter n (AdjoinRoot.root (cyclotomic n A))
          (RamifiedConjugation.root_pow_order A n) (Multiplicative.ofAdd a)) := by
…

Mentions: OAI.CirculantHadamard.CyclicPolynomial.powerCharacter, OAI.CirculantHadamard.RamifiedConjugation.root_pow_order, OAI.CirculantHadamard.RamifiedConjugation.cyclotomicConjugation

theorem OAI.CirculantHadamard.integerCyclotomicEvaluation_ringStar line 81
Source documentation
Evaluating the integer cyclic involution is exactly the cyclotomic conjugate of the evaluated element.
```
theorem integerCyclotomicEvaluation_ringStar (T : CyclicRing.Elem ℤ n) :
    integerCyclotomicEvaluation A n (CyclicRing.ringStar T) =
      RamifiedConjugation.cyclotomicConjugation A n hn
        (integerCyclotomicEvaluation A n T) := by
…
```
Mentions: OAI.CirculantHadamard.CyclicRing.Elem, OAI.CirculantHadamard.integerCyclotomicEvaluation, OAI.CirculantHadamard.CyclicRing.ringStar, OAI.CirculantHadamard.RamifiedConjugation.cyclotomicConjugation
theorem OAI.CirculantHadamard.integerCyclotomicEvaluation_norm line 96
Source documentation
A proved scalar norm equation in the integer group ring transfers to the actual cyclotomic norm equation.
```
theorem integerCyclotomicEvaluation_norm (T : CyclicRing.Elem ℤ n) (a : ℤ)
    (hT : T * CyclicRing.ringStar T = CyclicRing.scalar n a) :
    integerCyclotomicEvaluation A n T *
      RamifiedConjugation.cyclotomicConjugation A n hn
        (integerCyclotomicEvaluation A n T) =
      (a : AdjoinRoot (cyclotomic n A)) := by
…
```
Mentions: OAI.CirculantHadamard.CyclicRing.Elem, OAI.CirculantHadamard.CyclicRing.ringStar, OAI.CirculantHadamard.CyclicRing.scalar, OAI.CirculantHadamard.integerCyclotomicEvaluation, OAI.CirculantHadamard.RamifiedConjugation.cyclotomicConjugation