`BookProof.DensitySpectral.bornKernel_row_sum` (U : Matrix.unitaryGroup n ℂ) (i : n) : ∑ j, bornKernel (U : Matrix n n ℂ) i j = 1

Initializing...

`BookProof.DensitySpectral.bornKernel_row_sum` (U : Matrix.unitaryGroup n ℂ) (i : n) : ∑ j, bornKernel (U : Matrix n n ℂ) i j = 1 · Prove2Me