Theorems · Theorem · field theory

adjoinRootXPowSubCEquiv_symm_eq_root

∀ {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)] {α : L}
  (hα : α ^ n = (algebraMap K L) a),
  (adjoinRootXPowSubCEquiv hζ H hα).symm α = AdjoinRoot.root (Polynomial.X ^ n - Polynomial.C a)

Defined in

Mathlib.FieldTheory.KummerExtension

Cited by

2 results in Mathlib

Foundations

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

Assumes

FieldFieldAlgebraPolynomial.IsSplittingField