`BookProof.DensitySpectral.density_eigenvalues_sum_one` {ρ : Matrix n n ℂ} (h : IsDensityMatrix ρ) : ∑ i, h.1.eigenvalues i = 1

Initializing...

`BookProof.DensitySpectral.density_eigenvalues_sum_one` {ρ : Matrix n n ℂ} (h : IsDensityMatrix ρ) : ∑ i, h.1.eigenvalues i = 1 · Prove2Me