`BookProof.ChapterA3.upsilonC_metric` (T : Matrix (Fin 2) (Fin 2) ℂ) (hT : T.det = 1) : (UpsilonC T)ᵀ * toC minkowskiMat * UpsilonC T = toC minkowskiMat

Initializing...

`BookProof.ChapterA3.upsilonC_metric` (T : Matrix (Fin 2) (Fin 2) ℂ) (hT : T.det = 1) : (UpsilonC T)ᵀ * toC minkowskiMat * UpsilonC T = toC minkowskiMat · Prove2Me