derivative_natCast_mul — Mathlib

English

Let R be a semiring and f a polynomial in R[X]. For every natural number n, the derivative of the constant polynomial n multiplied by f equals n times the derivative of f:

Русский

Пусть R — полукольцо и f — многочлен над R. Для любого натурального числа n, производная от (n как константного многочлена) умноженного на f равна n умноженному на производную f.

LaTeX

$$$$ \operatorname{derivative}((n : R[X]) \cdot f) = n \cdot \operatorname{derivative} f $$$$

Lean4

theorem derivative_natCast_mul {n : ℕ} {f : R[X]} : derivative ((n : R[X]) * f) = n * derivative f := by simp

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