English
If R is a semiring and M is an additive commutative monoid with an R-module structure, ArithmeticFunction R acts as an R-module over ArithmeticFunction M.
Русский
Если R — полускольцо и M — аддитивный коммутативный моноид с модулем над R, то ArithmeticFunction R действует как модуль над ArithmeticFunction M.
LaTeX
$$Instance [Module (ArithmeticFunction R) (ArithmeticFunction M)]$$
Lean4
instance {M : Type*} [Semiring R] [AddCommMonoid M] [Module R M] : Module (ArithmeticFunction R) (ArithmeticFunction M)
where
one_smul := one_smul'
mul_smul := mul_smul'
smul_add r x
y := by
ext
simp only [sum_add_distrib, smul_add, smul_apply, add_apply]
smul_zero
r := by
ext
simp only [smul_apply, sum_const_zero, smul_zero, zero_apply]
add_smul r s
x := by
ext
simp only [add_smul, sum_add_distrib, smul_apply, add_apply]
zero_smul
r := by
ext
simp only [smul_apply, sum_const_zero, zero_smul, zero_apply]
