isConjRoot_of_aeval_eq_zero — Mathlib

English

If s1 and s2 are R-algebra isomorphisms, then s1 x and s2 x are conjugate roots.

Русский

Если s1 и s2 — R-алгебра изоморфизмы, то s1 x и s2 x — сопряжённые корни.

LaTeX

$$$IsConjRoot(R, s1(x), s2(x))$$$

Lean4

/-- Let `p` be the minimal polynomial of an integral element `x`. If `p y` = 0, then `y` is a
conjugate root of `x`.
-/
theorem isConjRoot_of_aeval_eq_zero [IsDomain A] {x y : A} (hx : IsIntegral K x) (h : aeval y (minpoly K x) = 0) :
    IsConjRoot K x y :=
  minpoly.eq_of_irreducible_of_monic (minpoly.irreducible hx) h (minpoly.monic hx)

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