`BookProof.ChapterAttentionCoarseGrain.sum_mergeWeights` (f : Fin m → Fin r) (p : Fin m → ℝ) : ∑ y, mergeWeights f p y = ∑ x, p x

Initializing...

`BookProof.ChapterAttentionCoarseGrain.sum_mergeWeights` (f : Fin m → Fin r) (p : Fin m → ℝ) : ∑ y, mergeWeights f p y = ∑ x, p x · Prove2Me