Theorems · Definition · commutative algebra

MvPolynomial.pderiv

{R : Type u} → {σ : Type v} → [inst : CommSemiring R] → σ → Derivation R (MvPolynomial σ R) (MvPolynomial σ R)

pderiv i p is the partial derivative of p with respect to i

Defined in

Mathlib.Algebra.MvPolynomial.PDeriv

Cited by

71 results in Mathlib

Foundations

Depth 93 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommSemiring