isConjRoot_iff_mem_minpoly_aroots

English

For IsIntegral x, IsConjRoot K x y iff y is in the roots of minpoly K x.

Русский

Для IsIntegral x, IsConjRoot K x y эквивалентно тому, что y принадлежит корням minpoly K x.

LaTeX

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

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_aroots {x y : S} (h : IsIntegral K x) :
    IsConjRoot K x y ↔ y ∈ (minpoly K x).aroots S :=
  by
  rw [Polynomial.mem_aroots, isConjRoot_iff_aeval_eq_zero h]
  simp only [iff_and_self]
  exact fun _ => minpoly.ne_zero h

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