Theorems · Theorem · commutative algebra

MvPolynomial.pderiv_rename

∀ {R : Type u} {σ : Type v} [inst : CommSemiring R] {τ : Type u_1} {f : σ → τ},
  Function.Injective f →
    ∀ (x : σ) (p : MvPolynomial σ R),
      (MvPolynomial.pderiv (f x)) ((MvPolynomial.rename f) p) = (MvPolynomial.rename f) ((MvPolynomial.pderiv x) p)

Defined in: Mathlib.Algebra.MvPolynomial.PDeriv
Cited by: 2 results in Mathlib
Foundations: Depth 96 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CommSemiring

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites22

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

DFunLike.coestatement and proof · cited by 62,936
CommSemiringstatement and proof · cited by 10,911
Finsuppstatement · cited by 5,255
mul_oneproof · cited by 3,885
AlgHomstatement · cited by 3,236
zero_addproof · cited by 2,366
MvPolynomialstatement and proof · cited by 2,140
MulZeroClass.mul_zeroproof · cited by 2,091
map_mulproof · cited by 1,137
map_addproof · cited by 964
MvPolynomial.Xproof · cited by 552
Derivationstatement · cited by 293

Cited by2

Results whose statement or proof uses this declaration.

Algebra.IsStandardSmoothOfRelativeDimension.exists_etale_mvPolynomialproof · cited by 1
Algebra.PreSubmersivePresentation.jacobiMatrix_reindexproof · cited by 1