Theorems · Theorem · field theory

autAdjoinRootXPowSubCEquiv_root

∀ {K : Type u} [inst : Field K] {n : ℕ} (hζ : (primitiveRoots n K).Nonempty) {a : K}
  (H : Irreducible (Polynomial.X ^ n - Polynomial.C a)) [inst_1 : NeZero n] (η : ↥(rootsOfUnity n K)),
  ((autAdjoinRootXPowSubCEquiv hζ H) η) (AdjoinRoot.root (Polynomial.X ^ n - Polynomial.C a)) =
    ↑↑η • AdjoinRoot.root (Polynomial.X ^ n - Polynomial.C a)

Defined in

Mathlib.FieldTheory.KummerExtension

Cited by

1 results in Mathlib

Foundations

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

Assumes

FieldNeZero