neg

Mathlib.FieldTheory.Minpoly.IsConjRoot

URI: https://scilib.ai/kg/mathlib#IsConjRoot.neg

← MathLib Explorer

English

If s is an algebra isomorphism, then x is a conjugate root of s x.

Русский

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

LaTeX

$$$IsConjRoot(R, x, (s\,x))$$$

Lean4

/-- If `y` is a conjugate root of `x`, then `-y` is a conjugate root of `-x`.
-/
theorem neg {x y : S} (h : IsConjRoot K x y) : IsConjRoot K (-x) (-y) := by
  rw [isConjRoot_def, minpoly.neg x, minpoly.neg y, h]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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