R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
x : ℕ
⊢ ∑ x in divisorsAntidiagonal x, ↑f x.fst * ↑↑ζ x.snd = ∑ i in divisors x, ↑f i
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
x : ℕ
⊢ ↑(f * ↑ζ) x = ∑ i in divisors x, ↑f i
rw [mul_apply]
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
x : ℕ
⊢ ∑ x in divisorsAntidiagonal x, ↑f x.fst * ↑↑ζ x.snd = ∑ i in divisorsAntidiagonal x, ↑f i.fst

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