finite_setOf_isRoot

Mathlib.Algebra.Polynomial.Roots

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

← MathLib Explorer

English

If p ≠ 0, then the set {x | IsRoot p x} is finite.

Русский

Если p ≠ 0, то множество {x | IsRoot p x} конечно.

LaTeX

$$Set.Finite {x | IsRoot p x} if p ≠ 0.$$

Lean4

theorem finite_setOf_isRoot {p : R[X]} (hp : p ≠ 0) : Set.Finite {x | IsRoot p x} := by
  classical simpa only [← Finset.setOf_mem, Multiset.mem_toFinset, mem_roots hp] using p.roots.toFinset.finite_toSet

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

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

Разделы

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

Аффилиация

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