`BookProof.SmBrstGhost.embedMatter_sum` {m : ℕ} {ι : Type*} (s : Finset ι) (M : ι → Matrix (Fin m) (Fin m) ℂ) : embedMatter m (∑ t ∈ s, M t) = ∑ t ∈ s, embedMatter m (M t)

Initializing...

`BookProof.SmBrstGhost.embedMatter_sum` {m : ℕ} {ι : Type*} (s : Finset ι) (M : ι → Matrix (Fin m) (Fin m) ℂ) : embedMatter m (∑ t ∈ s, M t) = ∑ t ∈ s, embedMatter m (M t) · Prove2Me