`BookProof.ChapterMaxEntropy.entropy_uniform` [Nonempty α] : entropy (uniform α) = Real.log (Fintype.card α)

Initializing...

`BookProof.ChapterMaxEntropy.entropy_uniform` [Nonempty α] : entropy (uniform α) = Real.log (Fintype.card α) · Prove2Me