`BookProof.ChapterGravityPolymomentum.metric_mul_metric` : metric * metric = (1 : Matrix (Fin 4) (Fin 4) ℝ)

Initializing...

`BookProof.ChapterGravityPolymomentum.metric_mul_metric` : metric * metric = (1 : Matrix (Fin 4) (Fin 4) ℝ) · Prove2Me