instCommRing — Mathlib

English

If R is a commutative ring and A is a nonunital commutative ring with Module structure, Unitization(R, A) is a commutative ring.

Русский

Если R — коммутативное кольцо, а A — коммутативное немонолитное кольцо, Unitization(R, A) является коммутативным кольцом.

LaTeX

$$$\text{CommRing}(\mathrm{Unitization}(R,A)).$$$

Lean4

instance instCommRing [CommRing R] [NonUnitalCommRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] :
    CommRing (Unitization R A) :=
  { Unitization.instAddCommGroup, Unitization.instCommSemiring with }

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