`BookProof.ChapterLorentzRealRepSum.gram_half10` : ∀ (i : Fin 4) (j : Fin 6), ((bHalf i)ᵀ * b10 j).trace = 0

Initializing...

`BookProof.ChapterLorentzRealRepSum.gram_half10` : ∀ (i : Fin 4) (j : Fin 6), ((bHalf i)ᵀ * b10 j).trace = 0 · Prove2Me