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

Initializing...

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