`BookProof.ChapterGravitySplit.timePart_eq_smul` (v x : Fin 4 → ℝ) : timePart v x = (-(minkForm x v)) • v

Initializing...

`BookProof.ChapterGravitySplit.timePart_eq_smul` (v x : Fin 4 → ℝ) : timePart v x = (-(minkForm x v)) • v · Prove2Me