`BookProof.ChapterLorentzRealRepFull.gram_two_10R` : ∀ (i : Fin 2) (j : Fin 6), ((w2R i)ᵀ * b10R j).trace = (0 : ℝ)

Initializing...

`BookProof.ChapterLorentzRealRepFull.gram_two_10R` : ∀ (i : Fin 2) (j : Fin 6), ((w2R i)ᵀ * b10R j).trace = (0 : ℝ) · Prove2Me