Theorems · Theorem · number theory

IsCyclotomicExtension.autEquivPow_apply

∀ {n : ℕ} [inst : NeZero n] {K : Type u_1} [inst_1 : Field K] (L : Type u_2) [inst_2 : CommRing L] [inst_3 : IsDomain L]
  [inst_4 : Algebra K L] [inst_5 : IsCyclotomicExtension {n} K L] (h : Irreducible (Polynomial.cyclotomic n K))
  (a : L ≃ₐ[K] L), (IsCyclotomicExtension.autEquivPow L h) a = (↑(IsPrimitiveRoot.autToPow K ⋯)).toFun a

Defined in

Mathlib.NumberTheory.Cyclotomic.Gal

Cited by

3 results in Mathlib

Foundations

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

Assumes

NeZeroFieldCommRingIsDomainAlgebraIsCyclotomicExtension