Theorems · Definition · number theory

IsCyclotomicExtension.autEquivPow

{n : ℕ} →
  [NeZero n] →
    {K : Type u_1} →
      [inst : Field K] →
        (L : Type u_2) →
          [inst_1 : CommRing L] →
            [IsDomain L] →
              [inst_3 : Algebra K L] →
                [IsCyclotomicExtension {n} K L] → Irreducible (Polynomial.cyclotomic n K) → (L ≃ₐ[K] L) ≃* (ZMod n)ˣ

The MulEquiv that takes an automorphism f to the element k : (ZMod n)ˣ such that f μ = μ ^ k for any root of unity μ. A strengthening of IsPrimitiveRoot.autToPow.

Defined in

Mathlib.NumberTheory.Cyclotomic.Gal

Cited by

3 results in Mathlib

Foundations

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

Assumes

NeZeroFieldCommRingIsDomainAlgebraIsCyclotomicExtension