`BookProof.SmBrstGhost.embedMatter_smul` (m : ℕ) (c : ℂ) (M : Matrix (Fin m) (Fin m) ℂ) : embedMatter m (c • M) = c • embedMatter m M

Initializing...

`BookProof.SmBrstGhost.embedMatter_smul` (m : ℕ) (c : ℂ) (M : Matrix (Fin m) (Fin m) ℂ) : embedMatter m (c • M) = c • embedMatter m M · Prove2Me