`BookProof.ChapterCoherentOccupation.coherentOccupation_hasSum_one` (lam : ℝ) : HasSum (coherentOccupation lam) 1

Initializing...

`BookProof.ChapterCoherentOccupation.coherentOccupation_hasSum_one` (lam : ℝ) : HasSum (coherentOccupation lam) 1 · Prove2Me