`BookProof.SmBrstGhost.embedMatter_sub` (m : ℕ) (M P : Matrix (Fin m) (Fin m) ℂ) : embedMatter m (M - P) = embedMatter m M

Initializing...

`BookProof.SmBrstGhost.embedMatter_sub` (m : ℕ) (M P : Matrix (Fin m) (Fin m) ℂ) : embedMatter m (M - P) = embedMatter m M - embedMatter m P · Prove2Me