`BookProof.ChapterLorentzTranslation.transPhase_rest` (M : ℝ) (x0 : ℝ) (xs : Fin 3 → ℝ) : transPhase M (fun _ => 0) x0 xs = Complex.exp (Complex.I * (M : ℂ) * (x0 : ℂ))

Initializing...

`BookProof.ChapterLorentzTranslation.transPhase_rest` (M : ℝ) (x0 : ℝ) (xs : Fin 3 → ℝ) : transPhase M (fun _ => 0) x0 xs = Complex.exp (Complex.I * (M : ℂ) * (x0 : ℂ)) · Prove2Me