`BookProof.ChapterLorentzRealRep.gram_10R` : ∀ i j : Fin 6, ((b10R i)ᵀ * b10R j).trace = if i = j then (4 : ℝ) else 0

Initializing...

`BookProof.ChapterLorentzRealRep.gram_10R` : ∀ i j : Fin 6, ((b10R i)ᵀ * b10R j).trace = if i = j then (4 : ℝ) else 0 · Prove2Me