polynomial_D_apply — Mathlib

English

For a polynomial P over R, the differential D applied to P equals the derivative of P times D applied to the variable X.

Русский

Для многочлена P над R дифференциал D(P) равен производной P, умноженной на D(X).

LaTeX

$$$D_{R,R[X]}(P) = (\\mathrm{derivative}\\ P) \\cdot D_{R,R[X]}(X).$$$

Lean4

theorem polynomial_D_apply (P : R[X]) : D R R[X] P = derivative P • D R R[X] X := by
  rw [← aeval_X_left_apply P, (D R R[X]).map_aeval, aeval_X_left_apply, aeval_X_left_apply]

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