Theorems · Theorem · commutative algebra

MvPolynomial.pderiv_sumRingEquiv

∀ {R : Type u} [inst : CommSemiring R] {σ : Type u_1} {ι : Type u_2} (p : MvPolynomial (σ ⊕ ι) R) (i : σ),
  (MvPolynomial.pderiv i) ((MvPolynomial.sumRingEquiv R σ ι) p) =
    (MvPolynomial.sumRingEquiv R σ ι) ((MvPolynomial.pderiv (Sum.inl i)) 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.

Cites25

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
zero_addproof · cited by 2,366
MvPolynomialstatement and proof · cited by 2,140
MulZeroClass.mul_zeroproof · cited by 2,091
map_zeroproof · cited by 1,614
RingEquivstatement · cited by 1,147
map_mulproof · cited by 1,137
map_addproof · cited by 964
MvPolynomial.Xproof · cited by 552

Cited by2

Results whose statement or proof uses this declaration.

MvPolynomial.pderiv_sumAlgEquivproof · cited by 1
MvPolynomial.pderiv_sumToIterproof · cited by 0