isConjRoot_iff_mem_minpoly_rootSet

English

For IsIntegral K x, IsConjRoot K x y iff y ∈ (minpoly K x).rootSet S.

Русский

Для IsIntegral K x, IsConjRoot K x y эквивалентно y ∈ (minpoly K x).rootSet S.

LaTeX

$$$IsConjRoot(K, x, y) \iff y \in (minpoly(K, x)).rootSet S$$$

Lean4

/-- `y` is a conjugate root of `x` over `K` if and only if `y` is a root of the minimal polynomial of
`x`. This is variant of `isConjRoot_iff_aeval_eq_zero`.
-/
theorem isConjRoot_iff_mem_minpoly_rootSet {x y : S} (h : IsIntegral K x) :
    IsConjRoot K x y ↔ y ∈ (minpoly K x).rootSet S :=
  (isConjRoot_iff_mem_minpoly_aroots h).trans (by simp [rootSet])

Похожие утверждения