Theorem: Sieve.selbergTerms_mult (PrimeNumberTheoremAnd/Mathlib/NumberTheory/Sieve/Basic.lean)

State before:
s : Sieve
⊢ g.IsMultiplicative
Tactic:
unfold selbergTerms
State after:
s : Sieve
⊢ (ν.pmul (ArithmeticFunction.prodPrimeFactors fun p => 1 / (1 - ν p))).IsMultiplicative

State before:
s : Sieve
⊢ (ν.pmul (ArithmeticFunction.prodPrimeFactors fun p => 1 / (1 - ν p))).IsMultiplicative
Tactic:
arith_mult
State after:
no goals