Theorem: SelbergSieve.mainSum_eq_diag_quad_form (PrimeNumberTheoremAnd/Mathlib/NumberTheory/Sieve/Selberg.lean)

State before:
s : SelbergSieve
⊢ s.mainSum μ⁺ = ∑ l ∈ P.divisors, 1 / g l * (∑ d ∈ P.divisors, if l ∣ d then ν d * s.selbergWeights d else 0) ^ 2
Tactic:
apply lambdaSquared_mainSum_eq_diag_quad_form
State after:
no goals