implicitDeriv — Mathlib

English

There exists a derivation on A[X] whose action on X is X′ and extends mapCoeffs with the derivative on A as coefficients.

Русский

Существует вывод на A[X], который действует на X как X′ и расширяет mapCoeffs, применяя к коэффициентам производную по A.

LaTeX

$$$\text{implicitDeriv}(X)=X'$, and $\text{implicitDeriv}(p)$ coincides with coefficientwise differentiation.$$

Lean4

/-- The unique derivation which can be made to a `DifferentialAlgebra` on `A[X]` with
`X′ = v`.
-/
def implicitDeriv (v : A[X]) : Derivation ℤ A[X] A[X] :=
  mapCoeffs + v • derivative'.restrictScalars ℤ

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