Theorem: LSeries.mul_mu_eq_one (EulerProducts/DirichletLSeries.lean)

State before:
φ : ℕ → ℂ
h₁ : φ 1 = 1
hφ : ∀ (m n : ℕ), φ (m * n) = φ m * φ n
s : ℂ
hs : LSeriesSummable φ s
⊢ L φ s * L (φ * fun n => ↑(μ n)) s = 1
Tactic:
rw [← LSeries_convolution' hs ?_, convolution_mul_moebius h₁ hφ, LSeries_delta, Pi.one_apply]
State after:
φ : ℕ → ℂ
h₁ : φ 1 = 1
hφ : ∀ (m n : ℕ), φ (m * n) = φ m * φ n
s : ℂ
hs : LSeriesSummable φ s
⊢ LSeriesSummable (φ * fun n => ↑(μ n)) s

State before:
φ : ℕ → ℂ
h₁ : φ 1 = 1
hφ : ∀ (m n : ℕ), φ (m * n) = φ m * φ n
s : ℂ
hs : LSeriesSummable φ s
⊢ LSeriesSummable (φ * fun n => ↑(μ n)) s
Tactic:
exact hs.mul_moebius
State after:
no goals