`BookProof.ChapterSternGerlach.exists_uniform_unitary` (n : ℕ) (hn : 0 < n) : ∃ U ∈ Matrix.unitaryGroup (Fin n) ℂ, ∀ i j : Fin n, Complex.normSq (U i j) = 1 / n

Initializing...

`BookProof.ChapterSternGerlach.exists_uniform_unitary` (n : ℕ) (hn : 0 < n) : ∃ U ∈ Matrix.unitaryGroup (Fin n) ℂ, ∀ i j : Fin n, Complex.normSq (U i j) = 1 / n · Prove2Me