rootMultiplicity_eq_zero

Mathlib.Algebra.Polynomial.Div

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

← MathLib Explorer

English

If p has no root at x, then rootMultiplicity x p = 0.

Русский

Если у p отсутствует корень в x, то rootMultiplicity x p = 0.

LaTeX

$$$ \neg \operatorname{IsRoot}(p,x) \Rightarrow \operatorname{rootMultiplicity}(x,p) = 0 $$$

Lean4

theorem rootMultiplicity_eq_zero {p : R[X]} {x : R} (h : ¬IsRoot p x) : rootMultiplicity x p = 0 :=
  rootMultiplicity_eq_zero_iff.2 fun h' => (h h').elim

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

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

Разделы

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

Аффилиация

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