`BookProof.ChapterLorentzRealRep.linIndep_of_gram` {n : ℕ} (v : Fin n → Matrix (Fin 4) (Fin 4) ℝ) (h : ∀ i j, ((v i)ᵀ * v j).trace = if i = j then (4 : ℝ) else 0) : LinearIndepende

Initializing...

`BookProof.ChapterLorentzRealRep.linIndep_of_gram` {n : ℕ} (v : Fin n → Matrix (Fin 4) (Fin 4) ℝ) (h : ∀ i j, ((v i)ᵀ * v j).trace = if i = j then (4 : ℝ) else 0) : LinearIndepende · Prove2Me