`BookProof.ChapterGravityMetric.spatialMetric_posSemidef` (v : Fin 4 → ℝ) (hv : minkSq v = -1) : (spatialMetric v).PosSemidef

Initializing...

`BookProof.ChapterGravityMetric.spatialMetric_posSemidef` (v : Fin 4 → ℝ) (hv : minkSq v = -1) : (spatialMetric v).PosSemidef · Prove2Me