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

State before:
φ : ℕ → ℂ
h₁ : φ 1 = 1
hφ : ∀ (m n : ℕ), φ (m * n) = φ m * φ n
this : (1 ⍟ fun x => ↑(μ x)) = δ
⊢ φ ⍟ (φ * fun n => ↑(μ n)) = δ
Tactic:
nth_rewrite 1 [← mul_one φ]
State after:
φ : ℕ → ℂ
h₁ : φ 1 = 1
hφ : ∀ (m n : ℕ), φ (m * n) = φ m * φ n
this : (1 ⍟ fun x => ↑(μ x)) = δ
⊢ φ * 1 ⍟ (φ * fun n => ↑(μ n)) = δ

State before:
φ : ℕ → ℂ
h₁ : φ 1 = 1
hφ : ∀ (m n : ℕ), φ (m * n) = φ m * φ n
this : (1 ⍟ fun x => ↑(μ x)) = δ
⊢ φ * 1 ⍟ (φ * fun n => ↑(μ n)) = δ
Tactic:
simp only [← mul_convolution_distrib hφ 1 ↗μ, this, mul_delta h₁]
State after:
no goals

State before:
φ : ℕ → ℂ
h₁ : φ 1 = 1
hφ : ∀ (m n : ℕ), φ (m * n) = φ m * φ n
⊢ (1 ⍟ fun x => ↑(μ x)) = δ
Tactic:
rw [one_convolution_eq_zeta_convolution, ← one_eq_delta]
State after:
φ : ℕ → ℂ
h₁ : φ 1 = 1
hφ : ∀ (m n : ℕ), φ (m * n) = φ m * φ n
⊢ ((fun x => ↑(ζ x)) ⍟ fun x => ↑(μ x)) = fun n => 1 n

State before:
φ : ℕ → ℂ
h₁ : φ 1 = 1
hφ : ∀ (m n : ℕ), φ (m * n) = φ m * φ n
⊢ ((fun x => ↑(ζ x)) ⍟ fun x => ↑(μ x)) = fun n => 1 n
Tactic:
change ⇑(ζ : ArithmeticFunction ℂ) ⍟ ⇑(μ : ArithmeticFunction ℂ) = ⇑(1 : ArithmeticFunction ℂ)
State after:
φ : ℕ → ℂ
h₁ : φ 1 = 1
hφ : ∀ (m n : ℕ), φ (m * n) = φ m * φ n
⊢ ⇑↑ζ ⍟ ⇑↑μ = ⇑1

State before:
φ : ℕ → ℂ
h₁ : φ 1 = 1
hφ : ∀ (m n : ℕ), φ (m * n) = φ m * φ n
⊢ ⇑↑ζ ⍟ ⇑↑μ = ⇑1
Tactic:
simp only [coe_mul, coe_zeta_mul_coe_moebius]
State after:
no goals