isConjRoot_def

Mathlib.FieldTheory.Minpoly.IsConjRoot

URI: https://scilib.ai/kg/mathlib#isConjRoot_def

English

IsConjRoot R x y is defined by the equivalence IsConjRoot R x y ≡ minpoly R x = minpoly R y.

Русский

IsConjRoot R x y задаётся эквивалентностью IsConjRoot R x y ≡ minpoly R x = minpoly R y.

LaTeX

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

Lean4

/-- The definition of conjugate roots.
-/
theorem isConjRoot_def {x y : A} : IsConjRoot R x y ↔ minpoly R x = minpoly R y :=
  Iff.rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru