Theorems · Theorem · field theory

autEquivRootsOfUnity_apply_rootOfSplit

∀ {K : Type u} [inst : Field K] {n : ℕ} (hζ : (primitiveRoots n K).Nonempty) {a : K}
  (H : Irreducible (Polynomial.X ^ n - Polynomial.C a)) (L : Type u_1) [inst_1 : Field L] [inst_2 : Algebra K L]
  [inst_3 : Polynomial.IsSplittingField K L (Polynomial.X ^ n - Polynomial.C a)] [inst_4 : NeZero n] (σ : Gal(L/K)),
  σ (rootOfSplitsXPowSubC ⋯ a L) = (autEquivRootsOfUnity hζ H L) σ • rootOfSplitsXPowSubC ⋯ a L

Defined in

Mathlib.FieldTheory.KummerExtension

Cited by

1 results in Mathlib

Foundations

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

Assumes

FieldFieldAlgebraPolynomial.IsSplittingFieldNeZero