instCommRingObjForget — Mathlib

English

For any commutative ring R, the underlying ring structure of R, viewed via the forgetful functor from commutative rings to rings, is again a commutative ring with the same operations.

Русский

У основания коммутативного кольца R через забывающее отображение от коммутативных колец к кольцам получается то же самое коммутативное кольцо на носителе R.

LaTeX

$$$ ((\\mathrm{forget} \\ \mathrm{CommRingCat}).\\mathrm{obj}\\ R) \\text{ carries a commutative ring structure; equivalently } \\mathrm{CommRing}(R).$$$

Lean4

instance {R : CommRingCat} : CommRing ((forget CommRingCat).obj R) :=
  (inferInstance : CommRing R.carrier)

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