rootMultiplicity_zero

Mathlib.Algebra.Polynomial.Div

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

English

The rootMultiplicity is zero when the second argument is free to vary or the polynomial is zero.

Русский

rootMultiplicity равна нулю в случаях, когда полином равен нулю или иное условие выполняется.

LaTeX

$$$$ \\operatorname{rootMultiplicity}(x, 0) = 0. $$$$

Lean4

@[simp]
theorem rootMultiplicity_zero {x : R} : rootMultiplicity x 0 = 0 :=
  dif_pos rfl

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

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

Разделы

Аффилиация

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