Theorems · Definition · number theory

IsPrimitiveRoot.subOnePowerBasis

{n : ℕ} →
  [NeZero n] →
    (K : Type u) →
      {L : Type v} →
        [inst : Field K] →
          [inst_1 : CommRing L] →
            [IsDomain L] →
              [inst_3 : Algebra K L] → [IsCyclotomicExtension {n} K L] → {ζ : L} → IsPrimitiveRoot ζ n → PowerBasis K L

The PowerBasis given by η - 1.

Defined in

Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots

Cited by

9 results in Mathlib

Foundations

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

Assumes

NeZeroFieldCommRingIsDomainAlgebraIsCyclotomicExtension