`BookProof.ChapterF1.ccr_mv` {n : ℕ} (i j : Fin n) (p : MvPolynomial (Fin n) ℂ) : (MvPolynomial.pderiv i) (MvPolynomial.X j * p) - MvPolynomial.X j * (MvPolynomial.pderiv i) p = (i

Initializing...

`BookProof.ChapterF1.ccr_mv` {n : ℕ} (i j : Fin n) (p : MvPolynomial (Fin n) ℂ) : (MvPolynomial.pderiv i) (MvPolynomial.X j * p) - MvPolynomial.X j * (MvPolynomial.pderiv i) p = (i · Prove2Me