instRing — Mathlib

English

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

Русский

Если R — коммутативное кольцо, а A — немонолитное кольцо с модулем, Unitization(R, A) образует кольцо.

LaTeX

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

Lean4

instance instRing [CommRing R] [NonUnitalRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] :
    Ring (Unitization R A) :=
  { Unitization.instAddCommGroup, Unitization.instSemiring with }

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