`BookProof.ChapterLorentzRealRep.castR_trace` (A : Matrix (Fin 4) (Fin 4) ℤ) : (castR A).trace = ((A.trace : ℤ) : ℝ)

Initializing...

`BookProof.ChapterLorentzRealRep.castR_trace` (A : Matrix (Fin 4) (Fin 4) ℤ) : (castR A).trace = ((A.trace : ℤ) : ℝ) · Prove2Me