English
For a fixed semiring R, ArithmeticFunction R carries a natural semiring structure.
Русский
Для фиксированного полускольного кольца R множество ArithmeticFunction R можно снабдить естественной структурой полускольца.
LaTeX
$$Instance: Semiring (ArithmeticFunction R)$$
Lean4
instance instSemiring : Semiring (ArithmeticFunction R) :=
{ ArithmeticFunction.instAddMonoidWithOne, ArithmeticFunction.instMonoid,
ArithmeticFunction.instAddCommMonoid with
zero_mul := fun f => by
ext
simp
mul_zero := fun f => by
ext
simp
left_distrib := fun a b c => by
ext
simp [← sum_add_distrib, mul_add]
right_distrib := fun a b c => by
ext
simp [← sum_add_distrib, add_mul] }