smulCommClass_left — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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