hasFDerivAt_aeval — Mathlib

English

For q ∈ Polynomial R and x ∈ 𝕜, HasFDerivAt of x ↦ AlgHom.coe (Polynomial.aeval x) q equals smulRight 1 (AlgHom.coe (Polynomial.aeval x) (derivative q)).

Русский

Для q ∈ Polynomial R и x ∈ 𝕜, коэффициентная производная HasFDerivAt от x ↦ AlgHom.coe(Polynomial.aeval x) q равна smulRight 1 (AlgHom.coe(Polynomial.aeval x)(derivative q)).

LaTeX

$$$HasFDerivAt\left(\lambda x, AlgHom.coe (Polynomial.aeval x) q\right)\left( smulRight\ 1\, (AlgHom.coe (Polynomial.aeval x) (derivative q))\right) x$$$

Lean4

protected theorem hasFDerivAt_aeval (x : 𝕜) :
    HasFDerivAt (fun x => aeval x q) (smulRight (1 : 𝕜 →L[𝕜] 𝕜) (aeval x (derivative q))) x :=
  q.hasDerivAt_aeval x

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