pderiv_pow

Mathlib.Algebra.MvPolynomial.PDeriv

URI: https://scilib.ai/kg/mathlib#MvPolynomial.pderiv_pow

← MathLib Explorer

English

The derivative of a power f^n is n · f^{n-1} · pderiv i f.

Русский

Производная степени f^n равна n · f^{n-1} · ∂_i f.

LaTeX

$$$$ pderiv(i)(f^n) = n \\cdot f^{n-1} \\cdot pderiv(i) f. $$$$

Lean4

theorem pderiv_pow {i : σ} {f : MvPolynomial σ R} {n : ℕ} : pderiv i (f ^ n) = n * f ^ (n - 1) * pderiv i f := by
  rw [(pderiv i).leibniz_pow f n, nsmul_eq_mul, smul_eq_mul, mul_assoc]

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

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

Разделы

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

Аффилиация

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