map_smul_of_tower — Mathlib

English

For a polynomial P with coefficients in R, D(aeval_x P) = aeval_x (derivative P) · D(x).

Русский

Для полинома P над R, выполняется D(aeval_x P) = aeval_x(derivative P) · D(x).

LaTeX

$$$D(\operatorname{aeval}_x P) = \operatorname{aeval}_x(\operatorname{derivative} P) \cdot D(x).$$$

Lean4

@[simp]
theorem map_smul_of_tower {S : Type*} [SMul S A] [SMul S M] [LinearMap.CompatibleSMul A M S R] (D : Derivation R A M)
    (r : S) (a : A) : D (r • a) = r • D a :=
  D.toLinearMap.map_smul_of_tower r a

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