`BookProof.ChapterAttentionQKCircuit.rank_qkMatrix_le` (WQ WK : Matrix (Fin d) (Fin n) ℝ) : (qkMatrix WQ WK).rank ≤ d

Initializing...

`BookProof.ChapterAttentionQKCircuit.rank_qkMatrix_le` (WQ WK : Matrix (Fin d) (Fin n) ℝ) : (qkMatrix WQ WK).rank ≤ d · Prove2Me