smulCommClass_right — Mathlib

English

The center of a semiring acts commutatively on the semiring from the right with respect to the multiplication.

Русский

Центр полусистемы действует коммутативно справа на самой системе по умножению.

LaTeX

$$$SMulCommClass\ R\ (center\ R)\ R$$$

Lean4

/-- The center of a semiring acts commutatively on that semiring. -/
instance smulCommClass_right : SMulCommClass R (center R) R :=
  Subsemiring.center.smulCommClass_right

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