Theorems · Theorem · field theory

notMem_iff_exists_ne_and_isConjRoot

∀ {K : Type u_2} {L : Type u_3} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] {x : L},
  IsSeparable K x → (Polynomial.map (algebraMap K L) (minpoly K x)).Splits → (x ∉ ⊥ ↔ ∃ y, x ≠ y ∧ IsConjRoot K x y)

Let L / K be a field extension. If x is a separable element over K and the minimal polynomial of x splits in L, then x is not in K if and only if there exists a conjugate root of x over K in L which is not equal to x itself.

Defined in

Mathlib.FieldTheory.Minpoly.IsConjRoot

Cited by

1 results in Mathlib

Foundations

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

Assumes

FieldFieldAlgebra