`BookProof.SmBrstGhost.embedMatter_row_ghost` (m : ℕ) (M : Matrix (Fin m) (Fin m) ℂ) (b : Fin 12) (j : Fin (m + 12)) : embedMatter m M (ghostMode m b) j = 0

Initializing...

`BookProof.SmBrstGhost.embedMatter_row_ghost` (m : ℕ) (M : Matrix (Fin m) (Fin m) ℂ) (b : Fin 12) (j : Fin (m + 12)) : embedMatter m M (ghostMode m b) j = 0 · Prove2Me