pderiv_X — Mathlib

English

The derivative of the variable X_j with respect to i is the indicator that i = j, i.e., pderiv i (X_j) is 1 if i = j and 0 otherwise.

Русский

Производная переменной X_j по i равна единице тогда и только тогда, когда i = j; иначе — ноль.

LaTeX

$$$$ pderiv(i)(X_j) = \\delta_{ij} = \\begin{cases} 1, & i=j \\\\ 0, & i\\neq j \\end{cases}. $$$$

Lean4

@[simp]
theorem pderiv_X [DecidableEq σ] (i j : σ) : pderiv i (X j : MvPolynomial σ R) = Pi.single (M := fun _ => _) i 1 j := by
  rw [pderiv_def, mkDerivation_X]

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