`BookProof.ChapterAttentionQKCircuit.qkScore_eq_bilinear` (WQ WK : Matrix (Fin d) (Fin n) ℝ) (x y : Fin n → ℝ) : qkScore WQ WK x y = x ⬝ᵥ (qkMatrix WQ WK *ᵥ y)

Initializing...

`BookProof.ChapterAttentionQKCircuit.qkScore_eq_bilinear` (WQ WK : Matrix (Fin d) (Fin n) ℝ) (x y : Fin n → ℝ) : qkScore WQ WK x y = x ⬝ᵥ (qkMatrix WQ WK *ᵥ y) · Prove2Me