`BookProof.ChapterSternGerlach.normSq_exp_mul_I` (θ : ℝ) : Complex.normSq (Complex.exp ((θ : ℂ) * Complex.I)) = 1

Initializing...

`BookProof.ChapterSternGerlach.normSq_exp_mul_I` (θ : ℝ) : Complex.normSq (Complex.exp ((θ : ℂ) * Complex.I)) = 1 · Prove2Me