pow_sub_dvd_iterate_derivative_pow

Mathlib.Algebra.Polynomial.Derivative

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

← MathLib Explorer

English

For p ∈ R[X], n,m ∈ ℕ, p^{n−m} ∣ derivative^[m](p^n).

Русский

Для p ∈ R[X], n,m ∈ ℕ, p^{n−m} делит derivative^[m](p^n).

LaTeX

$$$$ p^{\,n-m} \mid \operatorname{derivative}^{m}(p^{n}) $$$$

Lean4

theorem pow_sub_dvd_iterate_derivative_pow (p : R[X]) (n m : ℕ) : p ^ (n - m) ∣ derivative^[m] (p ^ n) :=
  pow_sub_dvd_iterate_derivative_of_pow_dvd m dvd_rfl

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

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

Разделы

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

Аффилиация

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