Theorems · Definition · number theory

IsPrimitiveRoot.integralPowerBasis

{n : ℕ} →
  {K : Type u} →
    [inst : Field K] →
      {ζ : K} →
        [NeZero n] →
          [inst_2 : CharZero K] →
            [IsCyclotomicExtension {n} ℚ K] → IsPrimitiveRoot ζ n → PowerBasis ℤ (NumberField.RingOfIntegers K)

The integral PowerBasis of 𝓞 K given by a primitive root of unity, where K is an n-th cyclotomic extension of ℚ.

Defined in

Mathlib.NumberTheory.NumberField.Cyclotomic.Basic

Cited by

3 results in Mathlib

Foundations

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

Assumes

FieldNeZeroCharZeroIsCyclotomicExtension