`BookProof.ChapterLorentzRealRep.conjL_apply` (S T A : Matrix (Fin 4) (Fin 4) ℝ) : conjL S T A = S * A * T

Initializing...

`BookProof.ChapterLorentzRealRep.conjL_apply` (S T A : Matrix (Fin 4) (Fin 4) ℝ) : conjL S T A = S * A * T · Prove2Me