instCommRing — Mathlib

English

The commutative semiring structure on ArithmeticFunction R satisfies the standard commutativity of multiplication with respect to addition in a defined sense.

Русский

Структура коммутативного полускольца на ArithmeticFunction R удовлетворяет стандартной коммутативности умножения относительно сложения.

LaTeX

$$proof: commutativity of multiplication in ArithmeticFunction R$$

Lean4

instance [CommRing R] : CommRing (ArithmeticFunction R) :=
  { ArithmeticFunction.instSemiring with
    neg_add_cancel := neg_add_cancel
    mul_comm := mul_comm
    zsmul := (· • ·) }

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