isConjRoot_iff_aeval_eq_zero — Mathlib

English

A conjugate root relation over Normal L/K is equivalent to the existence of a K-automorphism σ with σ(y) = x.

Русский

Относительная сопряжённость над нормальным расширением эквивалентна существованию K-автоморфизма σ с σ(y) = x.

LaTeX

$$$IsConjRoot(K, x, y) \iff \exists \sigma : L \cong_K L, \sigma(y) = x$$$

Lean4

/-- Let `p` be the minimal polynomial of an integral element `x`. Then `y` is a conjugate root of `x`
if and only if `p y = 0`.
-/
theorem isConjRoot_iff_aeval_eq_zero [IsDomain A] {x y : A} (h : IsIntegral K x) :
    IsConjRoot K x y ↔ aeval y (minpoly K x) = 0 :=
  ⟨IsConjRoot.aeval_eq_zero, isConjRoot_of_aeval_eq_zero h⟩

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