Theorem: LSeriesSummable.mul_moebius (EulerProducts/DirichletLSeries.lean)

State before:
f : ℕ → ℂ
s : ℂ
hf : LSeriesSummable f s
⊢ LSeriesSummable (f * fun n => ↑(μ n)) s
Tactic:
refine hf.mul_bounded (c := 1) fun n ↦ ?_
State after:
f : ℕ → ℂ
s : ℂ
hf : LSeriesSummable f s
n : ℕ
⊢ ‖↑(μ n)‖ ≤ 1

State before:
f : ℕ → ℂ
s : ℂ
hf : LSeriesSummable f s
n : ℕ
⊢ ‖↑(μ n)‖ ≤ 1
Tactic:
simp only [Complex.norm_int]
State after:
f : ℕ → ℂ
s : ℂ
hf : LSeriesSummable f s
n : ℕ
⊢ |↑(μ n)| ≤ 1

State before:
f : ℕ → ℂ
s : ℂ
hf : LSeriesSummable f s
n : ℕ
⊢ |↑(μ n)| ≤ 1
Tactic:
exact_mod_cast abs_moebius_le_one
State after:
no goals