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

Initializing...

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