`BookProof.QgCouplingDGammaSum.isHermCol_add` {a b : ℕ → (ℕ →₀ ℂ)} (ha : IsHermCol a) (hb : IsHermCol b) : IsHermCol (fun k => a k + b k)

Initializing...

`BookProof.QgCouplingDGammaSum.isHermCol_add` {a b : ℕ → (ℕ →₀ ℂ)} (ha : IsHermCol a) (hb : IsHermCol b) : IsHermCol (fun k => a k + b k) · Prove2Me