`BookProof.ChapterGravityPolymomentum.vecMulVec_mul` (w u : Fin 4 → ℝ) (M : Matrix (Fin 4) (Fin 4) ℝ) : vecMulVec w u * M = vecMulVec w (M.vecMul u)

Initializing...

`BookProof.ChapterGravityPolymomentum.vecMulVec_mul` (w u : Fin 4 → ℝ) (M : Matrix (Fin 4) (Fin 4) ℝ) : vecMulVec w u * M = vecMulVec w (M.vecMul u) · Prove2Me