`BookProof.ChapterLorentzRealRepSum.gram_10PsR` : ∀ (i : Fin 6) (j : Fin 4), ((b10R i)ᵀ * bPsR j).trace = (0 : ℝ)

Initializing...

`BookProof.ChapterLorentzRealRepSum.gram_10PsR` : ∀ (i : Fin 6) (j : Fin 4), ((b10R i)ᵀ * bPsR j).trace = (0 : ℝ) · Prove2Me