instCommSemiring — Mathlib

English

If R is a commutative semiring, then ArithmeticFunction R inherits a commutative semiring structure.

Русский

Если R — коммутативное полускольцо, то ArithmeticFunction R наследует коммутативное полускольцо.

LaTeX

$$Instance [CommSemiring R] : CommSemiring (ArithmeticFunction R)$$

Lean4

instance [CommSemiring R] : CommSemiring (ArithmeticFunction R) :=
  { ArithmeticFunction.instSemiring with
    mul_comm := fun f g => by
      ext
      rw [mul_apply, ← map_swap_divisorsAntidiagonal, sum_map]
      simp [mul_comm] }

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