`BookProof.ShiftedQuadratic.pgFunT_momTPoly_sq` (a k : Vd d) (i : Fin d) (p : MvPolynomial (Fin d) ℂ) (x : Vd d) : pgFunT a k (momTPoly k i (momTPoly k i p)) x = -deriv (fun t : ℝ

Initializing...

`BookProof.ShiftedQuadratic.pgFunT_momTPoly_sq` (a k : Vd d) (i : Fin d) (p : MvPolynomial (Fin d) ℂ) (x : Vd d) : pgFunT a k (momTPoly k i (momTPoly k i p)) x = -deriv (fun t : ℝ · Prove2Me