`BookProof.ChapterGravityPolymomentum.proj_metric` (v : Fin 4 → ℝ) (hv : minkSq v = -1) : proj v metric = metric + vecMulVec v v

Initializing...

`BookProof.ChapterGravityPolymomentum.proj_metric` (v : Fin 4 → ℝ) (hv : minkSq v = -1) : proj v metric = metric + vecMulVec v v · Prove2Me