f g : ArithmeticFunction ℂ
z : ℂ
hf : LSeriesSummable f z
hg : LSeriesSummable g z
⊢ (∑' (n : ℕ), (↑f n + ↑g n) / ↑n ^ z) = (∑' (n : ℕ), ↑f n / ↑n ^ z) + ∑' (n : ℕ), ↑g n / ↑n ^ z
f g : ArithmeticFunction ℂ
z : ℂ
hf : LSeriesSummable f z
hg : LSeriesSummable g z
⊢ LSeries (f + g) z = LSeries f z + LSeries g z
simp only [LSeries, add_apply]
f g : ArithmeticFunction ℂ
z : ℂ
hf : LSeriesSummable f z
hg : LSeriesSummable g z
⊢ (∑' (n : ℕ), (↑f n + ↑g n) / ↑n ^ z) = ∑' (b : ℕ), ↑f b / ↑b ^ z + ↑g b / ↑b ^ z
f g : ArithmeticFunction ℂ
z : ℂ
hf : LSeriesSummable f z
hg : LSeriesSummable g z
⊢ (∑' (n : ℕ), (↑f n + ↑g n) / ↑n ^ z) = (∑' (n : ℕ), ↑f n / ↑n ^ z) + ∑' (n : ℕ), ↑g n / ↑n ^ z
rw [← tsum_add hf hg]
f g : ArithmeticFunction ℂ
z : ℂ
hf : LSeriesSummable f z
hg : LSeriesSummable g z
⊢ ∀ (n : ℕ), (↑f n + ↑g n) / ↑n ^ z = ↑f n / ↑n ^ z + ↑g n / ↑n ^ z
f g : ArithmeticFunction ℂ
z : ℂ
hf : LSeriesSummable f z
hg : LSeriesSummable g z
⊢ (∑' (n : ℕ), (↑f n + ↑g n) / ↑n ^ z) = ∑' (b : ℕ), ↑f b / ↑b ^ z + ↑g b / ↑b ^ z
apply congr rfl (funext fun n => _)
no goals
f g : ArithmeticFunction ℂ
z : ℂ
hf : LSeriesSummable f z
hg : LSeriesSummable g z
⊢ ∀ (n : ℕ), (↑f n + ↑g n) / ↑n ^ z = ↑f n / ↑n ^ z + ↑g n / ↑n ^ z
simp [_root_.add_div]