`BookProof.ChapterGravityPolymomentum.metric_mulVec_lower` (v : Fin 4 → ℝ) : metric.mulVec (lower v) = v

Initializing...

`BookProof.ChapterGravityPolymomentum.metric_mulVec_lower` (v : Fin 4 → ℝ) : metric.mulVec (lower v) = v · Prove2Me