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

Initializing...

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