pderiv_monomial_single — Mathlib

English

The derivative of the monomial monomial(single i n) a with respect to i is monomial(single i (n-1)) (a n).

Русский

Производная мономиала (single i n) a по i равна мономиалу (single i (n-1)) (a n).

LaTeX

$$$$ pderiv(i)(monomial(\\text{single}(i,n), a)) = monomial(\\text{single}(i,(n-1)), a \\cdot n). $$$$

Lean4

theorem pderiv_monomial_single {i : σ} {n : ℕ} :
    pderiv i (monomial (single i n) a) = monomial (single i (n - 1)) (a * n) := by simp

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