forgetToTopCatCommRing — Mathlib

English

On an object R of TopCommRingCat, the underlying ring structure on the forgetful image is a commutative ring.

Русский

У носителя в образе, попавшем под забывающую▽ функцию на TopCat, имеется структура коммутативного кольца.

LaTeX

$$$\text{forget₂ TopCommRingCat TopCat}(R)\text{ carries a } \mathrm{CommRing}.$$$

Lean4

instance forgetToTopCatCommRing (R : TopCommRingCat) : CommRing ((forget₂ TopCommRingCat TopCat).obj R) :=
  R.isCommRing

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