derivative_C_mul

Mathlib.Algebra.Polynomial.Derivative

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

English

For any a ∈ R and polynomial p ∈ R[X], derivative(C a · p) = C a · derivative p.

Русский

Для любого a ∈ R и многочлена p ∈ R[X] производная(C a · p) = C a · производная p.

LaTeX

$$$\operatorname{derivative}(C a \cdot p) = C a \cdot \operatorname{derivative}(p)$$$

Lean4

theorem derivative_C_mul (a : R) (p : R[X]) : derivative (C a * p) = C a * derivative p :=
  iterate_derivative_C_mul _ _ 1

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

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

Разделы

Аффилиация

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