pderiv_C_mul — Mathlib

English

The derivative distributes over a constant multiplier: pderiv i (C a · f) = C a · pderiv i f.

Русский

Производная константного множителя равна константному множителю times производная: ∂_i(Ca f) = Ca ∂_i f.

LaTeX

$$$$ pderiv(i)(C a \\cdot f) = C a \\cdot pderiv(i) f. $$$$

Lean4

theorem pderiv_C_mul {f : MvPolynomial σ R} {i : σ} : pderiv i (C a * f) = C a * pderiv i f := by
  rw [C_mul', Derivation.map_smul, C_mul']

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