`BookProof.ChapterAttentionEntropy.shannonEntropy_uniform` (hm : 0 < m) : shannonEntropy (fun _ : Fin m => (1 : ℝ) / m) = Real.log m

Initializing...

`BookProof.ChapterAttentionEntropy.shannonEntropy_uniform` (hm : 0 < m) : shannonEntropy (fun _ : Fin m => (1 : ℝ) / m) = Real.log m · Prove2Me