instNonUnitalCommRing — Mathlib

English

The center is a nonunital commutative ring (in particular, commutative under multiplication).

Русский

Центр образует ненумитное коммутативное кольцо (в частности, умножение коммутативно).

LaTeX

$$center R A is a NonUnitalCommRing$$

Lean4

instance instNonUnitalCommRing {A : Type*} [NonUnitalNonAssocRing A] [Module R A] [IsScalarTower R A A]
    [SMulCommClass R A A] : NonUnitalCommRing (center R A) :=
  NonUnitalSubring.center.instNonUnitalCommRing _

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