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

Initializing...

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