instSemiring — Mathlib

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] }

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