`BookProof.ShiftedQuadraticDegenerate.diagonal_mulVec_diagShiftVec` {c w : Fin d → ℝ} (hcw : ∀ i, c i = 0 → w i = 0) (i : Fin d) : ∑ j, (Matrix.diagonal c) i j * (diagShiftVec c w)

Initializing...

`BookProof.ShiftedQuadraticDegenerate.diagonal_mulVec_diagShiftVec` {c w : Fin d → ℝ} (hcw : ∀ i, c i = 0 → w i = 0) (i : Fin d) : ∑ j, (Matrix.diagonal c) i j * (diagShiftVec c w) · Prove2Me