derivative_X_sub_C_sq

Mathlib.Algebra.Polynomial.Derivative

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

English

Derivative of X − C c squared is C(2) · (X − C c).

Русский

Производная от (X − C c)^2 равна C(2) · (X − C c).

LaTeX

$$$\operatorname{derivative}(X - C c)^{2} = C(2) \cdot (X - C c)$$$

Lean4

theorem derivative_X_sub_C_sq (c : R) : derivative ((X - C c) ^ 2) = C 2 * (X - C c) := by
  rw [derivative_sq, derivative_X_sub_C, mul_one]

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

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

Разделы

Аффилиация

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