derivative_C_mul_X_sq — Mathlib

English

For a ∈ A and d a derivation, d(aeval a f) = aeval a (derivative f) · d a for all f ∈ R[X].

Русский

Для a ∈ A и деривации d, верно d(aeval a f) = aeval a (derivative f) · d a для всех f ∈ R[X].

LaTeX

$$$d(\\mathrm{aeval}\\ a\\; f) = \\mathrm{aeval}\\ a\\ (\\operatorname{derivative}(f)) \\cdot d a.$$$

Lean4

theorem derivative_C_mul_X_sq (a : R) : derivative (C a * X ^ 2) = C (a * 2) * X := by
  rw [derivative_C_mul_X_pow, Nat.cast_two, pow_one]

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