pderiv — Mathlib

English

For any R and σ, pderiv i is the R-derivation on MvPolynomial σ R determined by the map sending i to 1 at the multi-index Pi.single i 1.

Русский

Для любых R и σ pderiv i — это R-производная на MvPolynomial σ R, определенная картой, посылающей i в Pi.single i 1.

LaTeX

$$$$ \\text{pderiv}(i) = \\operatorname{mkDerivation}(R, \\Pi.single(i,1)). $$$$

Lean4

/-- `pderiv i p` is the partial derivative of `p` with respect to `i` -/
def pderiv (i : σ) : Derivation R (MvPolynomial σ R) (MvPolynomial σ R) :=
  letI := Classical.decEq σ
  mkDerivation R <| Pi.single i 1

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