`BookProof.QgCouplingDGammaSum.isPosCol_diagCol` {lam : ℕ → ℝ} (hlam : ∀ k, 0 ≤ lam k) : IsPosCol (diagCol lam)

Initializing...

`BookProof.QgCouplingDGammaSum.isPosCol_diagCol` {lam : ℕ → ℝ} (hlam : ∀ k, 0 ≤ lam k) : IsPosCol (diagCol lam) · Prove2Me