R : Type u_2
M : Type u_1
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : ArithmeticFunction M
x : ℕ
⊢ ∑ x in divisorsAntidiagonal x, ↑↑ζ x.fst • ↑f x.snd = ∑ i in divisors x, ↑f i
R : Type u_2
M : Type u_1
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : ArithmeticFunction M
x : ℕ
⊢ ↑(↑ζ • f) x = ∑ i in divisors x, ↑f i
rw [smul_apply]
R : Type u_2
M : Type u_1
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : ArithmeticFunction M
x : ℕ
⊢ ∑ x in divisorsAntidiagonal x, ↑↑ζ x.fst • ↑f x.snd = ∑ i in divisorsAntidiagonal x, ↑f i.snd

R : Type u_2
M : Type u_1
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : ArithmeticFunction M
x : ℕ
⊢ ∑ i in divisorsAntidiagonal x, ↑f i.snd = ∑ i in divisors x, ↑f i
R : Type u_2
M : Type u_1
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : ArithmeticFunction M
x : ℕ
⊢ ∑ x in divisorsAntidiagonal x, ↑↑ζ x.fst • ↑f x.snd = ∑ i in divisors x, ↑f i
trans ∑ i in divisorsAntidiagonal x, f i.snd
R : Type u_2
M : Type u_1
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : ArithmeticFunction M
x : ℕ
i : ℕ × ℕ
hi : i ∈ divisorsAntidiagonal x
⊢ ↑↑ζ i.fst • ↑f i.snd = ↑f i.snd
R : Type u_2
M : Type u_1
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : ArithmeticFunction M
x : ℕ
⊢ ∑ x in divisorsAntidiagonal x, ↑↑ζ x.fst • ↑f x.snd = ∑ i in divisorsAntidiagonal x, ↑f i.snd
refine' sum_congr rfl fun i hi => _
case intro
R : Type u_2
M : Type u_1
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : ArithmeticFunction M
i : ℕ × ℕ
hi : i ∈ divisorsAntidiagonal (i.fst * i.snd)
h : i.fst * i.snd ≠ 0
⊢ ↑↑ζ i.fst • ↑f i.snd = ↑f i.snd
R : Type u_2
M : Type u_1
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : ArithmeticFunction M
x : ℕ
i : ℕ × ℕ
hi : i ∈ divisorsAntidiagonal x
⊢ ↑↑ζ i.fst • ↑f i.snd = ↑f i.snd
rcases mem_divisorsAntidiagonal.1 hi with ⟨rfl, h⟩
no goals
case intro
R : Type u_2
M : Type u_1
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : ArithmeticFunction M
i : ℕ × ℕ
hi : i ∈ divisorsAntidiagonal (i.fst * i.snd)
h : i.fst * i.snd ≠ 0
⊢ ↑↑ζ i.fst • ↑f i.snd = ↑f i.snd
rw [natCoe_apply, zeta_apply_ne (left_ne_zero_of_mul h), cast_one, one_smul]
no goals
R : Type u_2
M : Type u_1
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : ArithmeticFunction M
x : ℕ
⊢ ∑ i in divisorsAntidiagonal x, ↑f i.snd = ∑ i in divisors x, ↑f i
rw [← map_div_left_divisors, sum_map, Function.Embedding.coeFn_mk]