rootSet_neg

Mathlib.Algebra.Polynomial.Roots

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

← MathLib Explorer

English

Root set is invariant under negation: rootSet(-p) = rootSet(p).

Русский

Корневое множество сохраняется при взятии отрицания: rootSet(-p) = rootSet(p).

LaTeX

$$$$ \mathrm{rootSet}(-p,S) = \mathrm{rootSet}(p,S) $$$$

Lean4

@[simp]
theorem rootSet_neg (p : T[X]) (S) [CommRing S] [IsDomain S] [Algebra T S] : (-p).rootSet S = p.rootSet S := by
  rw [rootSet, aroots_neg, rootSet]

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

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

Разделы

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

Аффилиация

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