Theorems · Theorem · field theory

autAdjoinRootXPowSubCEquiv_symm_smul

∀ {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]
  (σ : AdjoinRoot (Polynomial.X ^ n - Polynomial.C a) ≃ₐ[K] AdjoinRoot (Polynomial.X ^ n - Polynomial.C a)),
  ↑((autAdjoinRootXPowSubCEquiv hζ H).symm σ) • AdjoinRoot.root (Polynomial.X ^ n - Polynomial.C a) =
    σ (AdjoinRoot.root (Polynomial.X ^ n - Polynomial.C a))

Defined in

Mathlib.FieldTheory.KummerExtension

Cited by

0 results in Mathlib

Foundations

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

Assumes

FieldNeZero