English
For Ring R, and f,g : ArithmeticFunction Int, we have (f * g).ofInt = (f.ofInt) * (g.ofInt).
Русский
Для кольца R и функций f,g : ArithmeticFunction Int выполняется (f * g).ofInt = (f.ofInt) * (g.ofInt).
LaTeX
$$$\\operatorname{ofInt}(f * g) = (\\operatorname{ofInt} f) * (\\operatorname{ofInt} g)$$$
Lean4
theorem mul_smul' (f g : ArithmeticFunction R) (h : ArithmeticFunction M) : (f * g) • h = f • g • h :=
by
ext n
simp only [mul_apply, smul_apply, sum_smul, mul_smul, smul_sum, Finset.sum_sigma']
apply
Finset.sum_nbij' (fun ⟨⟨_i, j⟩, ⟨k, l⟩⟩ ↦ ⟨(k, l * j), (l, j)⟩) (fun ⟨⟨i, _j⟩, ⟨k, l⟩⟩ ↦ ⟨(i * k, l), (i, k)⟩) <;>
aesop (add simp mul_assoc)