derivative_X_add_C_pow — Mathlib

English

Let R be a commutative semiring and c ∈ R. For any natural m, the derivative with respect to X of (X + C c)^m is the constant polynomial C(m) multiplied by (X + C c)^{m−1}. In other words, d/dX (X + C c)^m = C(m) · (X + C c)^{m−1}.

Русский

Пусть R — коммутативное полугруппа, c ∈ R. Для любого натурального m производная по X от (X + C c)^m равна константному полиному C(m) умноженному на (X + C c)^{m−1}. Иными словами, d/dX (X + C c)^m = C(m) · (X + C c)^{m−1}.

LaTeX

$$$\operatorname{derivative}((X+C c)^m) = C(m) \cdot (X+C c)^{m-1}$$$

Lean4

theorem derivative_X_add_C_pow (c : R) (m : ℕ) : derivative ((X + C c) ^ m) = C (m : R) * (X + C c) ^ (m - 1) := by
  rw [derivative_pow, derivative_X_add_C, mul_one]

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