derivative_smul — Mathlib

English

Let S act on R[X] via scalar multiplication, with appropriate compatibility. Then the derivative is linear over the scalar: derivative(s · p) = s · derivative(p).

Русский

Пусть S действует на R[X] скаляром и выполняются соответствующие условия. Тогда производная линейна по скаляру: производная(i) s · p = s · производная(p).

LaTeX

$$$\operatorname{derivative}(s \cdot p) = s \cdot \operatorname{derivative}(p)$$$

Lean4

theorem derivative_smul {S : Type*} [SMulZeroClass S R] [IsScalarTower S R R] (s : S) (p : R[X]) :
    derivative (s • p) = s • derivative p :=
  derivative.map_smul_of_tower s p

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