Theorems · Definition · number theory

IsPrimitiveRoot.integralPowerBasisOfPrimePow

{p k : ℕ} →
  {K : Type u} →
    [inst : Field K] →
      {ζ : K} →
        [hp : Fact (Nat.Prime p)] →
          [inst_1 : CharZero K] →
            [IsCyclotomicExtension {p ^ k} ℚ K] →
              IsPrimitiveRoot ζ (p ^ k) → PowerBasis ℤ (NumberField.RingOfIntegers K)

The integral PowerBasis of 𝓞 K given by a primitive root of unity, where K is a p ^ k cyclotomic extension of ℚ.

Defined in

Mathlib.NumberTheory.NumberField.Cyclotomic.Basic

Cited by

6 results in Mathlib

Foundations

Depth 224 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FieldFactCharZeroIsCyclotomicExtension