`BookProof.ChapterAttentionOVCircuit.ovOutput_eq_headOutput` (beta : ℝ) (s : Fin m → ℝ) (WO : Matrix (Fin n) (Fin d) ℝ) (WV : Matrix (Fin d) (Fin n) ℝ) (x : Fin m → (Fin n → ℝ)) :

Initializing...

`BookProof.ChapterAttentionOVCircuit.ovOutput_eq_headOutput` (beta : ℝ) (s : Fin m → ℝ) (WO : Matrix (Fin n) (Fin d) ℝ) (WV : Matrix (Fin d) (Fin n) ℝ) (x : Fin m → (Fin n → ℝ)) : · Prove2Me