`BookProof.ChapterGravityPolymomentum.proj_eq_self_of_spatial` (v : Fin 4 → ℝ) {M : Matrix (Fin 4) (Fin 4) ℝ} (h : IsSpatial v M) : proj v M = M

Initializing...

`BookProof.ChapterGravityPolymomentum.proj_eq_self_of_spatial` (v : Fin 4 → ℝ) {M : Matrix (Fin 4) (Fin 4) ℝ} (h : IsSpatial v M) : proj v M = M · Prove2Me