`BookProof.ChapterGravityMetric.spatialMetric_quadForm_nonneg` (v x : Fin 4 → ℝ) (hv : minkSq v = -1) : 0 ≤ x ⬝ᵥ ((spatialMetric v).mulVec x)

Initializing...

`BookProof.ChapterGravityMetric.spatialMetric_quadForm_nonneg` (v x : Fin 4 → ℝ) (hv : minkSq v = -1) : 0 ≤ x ⬝ᵥ ((spatialMetric v).mulVec x) · Prove2Me