IsConjRoot — Mathlib

English

Conjugate roots are defined by equality of minimal polynomials: y is a conjugate root of x over K if and only if minpoly R x = minpoly R y.

Русский

Сопряжённые корни определяются равенством минимальных многочленов: y является сопряжённым корнем x над K тогда и только тогда minpoly R x = minpoly R y.

LaTeX

$$$\text{IsConjRoot}(R, x, y) \iff \minpoly(R, x) = \minpoly(R, y)$$$

Lean4

/-- We say that `y` is a conjugate root of `x` over `K` if the minimal polynomial of `x` is the
same as the minimal polynomial of `y`.
-/
def IsConjRoot (x y : A) : Prop :=
  minpoly R x = minpoly R y

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