(i : Fin 3) (p : MvPolynomial (Fin 3) ℂ) : momPoly i (momPoly i p) + mulXPoly i (mulXPoly i (((1 / 4 : ℂ)) • p)) = crePoly i (annPoly i p) + ((1 / 2 : ℂ)) • p

Initializing...

(i : Fin 3) (p : MvPolynomial (Fin 3) ℂ) : momPoly i (momPoly i p) + mulXPoly i (mulXPoly i (((1 / 4 : ℂ)) • p)) = crePoly i (annPoly i p) + ((1 / 2 : ℂ)) • p · Prove2Me