aroots_neg

Mathlib.Algebra.Polynomial.Roots

URI: https://scilib.ai/kg/mathlib#Polynomial.aroots_neg

← MathLib Explorer

English

The roots of a polynomial and its negation coincide.

Русский

Корни многочлена и его отрицания совпадают.

LaTeX

$$$$ \operatorname{aroots}_S(-p) = \operatorname{aroots}_S(p) $$$$

Lean4

@[simp]
theorem aroots_neg [CommRing S] [IsDomain S] [Algebra T S] (p : T[X]) : (-p).aroots S = p.aroots S := by
  rw [aroots, Polynomial.map_neg, roots_neg]

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

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

Разделы

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

Аффилиация

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