`BookProof.ChapterIrreversible.bornDist_sum` (v : Fin n → ℂ) (hv : ∑ a, ‖v a‖ ^ 2 = 1) : ∑ a, bornDist v a = 1

Initializing...

`BookProof.ChapterIrreversible.bornDist_sum` (v : Fin n → ℂ) (hv : ∑ a, ‖v a‖ ^ 2 = 1) : ∑ a, bornDist v a = 1 · Prove2Me