Theorems · Theorem · commutative algebra

MvPolynomial.pderiv_map

∀ {R : Type u} {σ : Type v} [inst : CommSemiring R] {S : Type u_1} [inst_1 : CommSemiring S] {φ : R →+* S}
  {f : MvPolynomial σ R} {i : σ},
  (MvPolynomial.pderiv i) ((MvPolynomial.map φ) f) = (MvPolynomial.map φ) ((MvPolynomial.pderiv i) f)

Defined in

Mathlib.Algebra.MvPolynomial.PDeriv

Cited by

8 results in Mathlib

Foundations

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

Assumes

CommSemiringCommSemiring