`BookProof.ChapterAngularMomentum.angularMomentum_eigen` {u : ℂ → ℂ} {μ : ℝ} {z : ℂ} (hdiff : DifferentiableAt ℝ u z) (hequiv : ∀ t : ℝ, u (Complex.exp ((t : ℂ) * Complex.I) * z) =

Initializing...

`BookProof.ChapterAngularMomentum.angularMomentum_eigen` {u : ℂ → ℂ} {μ : ℝ} {z : ℂ} (hdiff : DifferentiableAt ℝ u z) (hequiv : ∀ t : ℝ, u (Complex.exp ((t : ℂ) * Complex.I) * z) = · Prove2Me