derivative_X_add_C_sq — Mathlib

English

Let R be a commutative semiring and c ∈ R. The derivative of (X + C c)^2 is C(2) · (X + C c).

Русский

Пусть R — коммутативное полугруппа и c ∈ R. Производная от (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_add_C_sq (c : R) : derivative ((X + C c) ^ 2) = C 2 * (X + C c) := by
  rw [derivative_sq, derivative_X_add_C, mul_one]

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