`BookProof.ChapterAttentionOutput.headOutput_eq_sum` (beta : ℝ) (s : Fin m → ℝ) (v : Fin m → E) : headOutput beta s v = ∑ j, scoreSoftmax beta s j • v j

Initializing...

`BookProof.ChapterAttentionOutput.headOutput_eq_sum` (beta : ℝ) (s : Fin m → ℝ) (v : Fin m → E) : headOutput beta s v = ∑ j, scoreSoftmax beta s j • v j · Prove2Me