`BookProof.ChapterAttentionOutput.headOutput_zero` (s : Fin m → ℝ) (v : Fin m → E) : headOutput 0 s v = ((m : ℝ))⁻¹ • ∑ j, v j

Initializing...

`BookProof.ChapterAttentionOutput.headOutput_zero` (s : Fin m → ℝ) (v : Fin m → E) : headOutput 0 s v = ((m : ℝ))⁻¹ • ∑ j, v j · Prove2Me