instMod

Mathlib.Algebra.Polynomial.FieldDivision

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

English

For CharZero R and p ≠ 0, we have: n < rootMultiplicity_t(p) iff ∀ m ≤ n, (derivative^m p).IsRoot t.

Русский

Для CharZero R и p ≠ 0 имеем: n < ord_t(p) тогда и только тогда, когда ∀ m ≤ n, (derivative^m p).IsRoot t.

LaTeX

$$$p \neq 0 \Rightarrow \Bigl(n < \operatorname{rootMultiplicity}_t(p) \iff \forall m \le n, (\operatorname{derivative}^{\,m} p).IsRoot t\Bigr).$$$

Lean4

instance : Mod R[X] :=
  ⟨mod⟩

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

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

Разделы

Аффилиация

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