`BookProof.ChapterGravityPolymomentum.mul_spatialProj_transpose` (v : Fin 4 → ℝ) (M : Matrix (Fin 4) (Fin 4) ℝ) : M * (spatialProj v)ᵀ = M + vecMulVec (M.mulVec (lower v)) v

Initializing...

`BookProof.ChapterGravityPolymomentum.mul_spatialProj_transpose` (v : Fin 4 → ℝ) (M : Matrix (Fin 4) (Fin 4) ℝ) : M * (spatialProj v)ᵀ = M + vecMulVec (M.mulVec (lower v)) v · Prove2Me