`BookProof.ChapterLorentzRealRepDirect.sum_finrank_WFam` : (∑ i, finrank ℝ (WFam i)) = finrank ℝ (Matrix (Fin 4) (Fin 4) ℝ)

Initializing...

`BookProof.ChapterLorentzRealRepDirect.sum_finrank_WFam` : (∑ i, finrank ℝ (WFam i)) = finrank ℝ (Matrix (Fin 4) (Fin 4) ℝ) · Prove2Me