`BookProof.ScalaronFock.inner_qgDir` (n : ℕ) (x : qgSector n) (j : Fin n) (i : Fin 2) : (inner ℝ x (qgDir n j i) : ℝ) = x (j, i)

Initializing...

`BookProof.ScalaronFock.inner_qgDir` (n : ℕ) (x : qgSector n) (j : Fin n) (i : Fin 2) : (inner ℝ x (qgDir n j i) : ℝ) = x (j, i) · Prove2Me