rootSet_C

Mathlib.Algebra.Polynomial.Roots

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

← MathLib Explorer

English

The root set of a constant polynomial C(a) is empty.

Русский

Множество корней константного многочлена C(a) пусто.

LaTeX

$$$$ (C(a)).rootSet S = \emptyset $$$$

Lean4

@[simp]
theorem rootSet_C [CommRing S] [IsDomain S] [Algebra T S] (a : T) : (C a).rootSet S = ∅ := by
  classical rw [rootSet_def, aroots_C, Multiset.toFinset_zero, Finset.coe_empty]

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

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

Разделы

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

Аффилиация

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