mul_smul' — Mathlib

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)

Похожие утверждения