instCommRingCarrierObjOppositeRingCatCompCommRingCatForget₂

Mathlib.Algebra.Category.ModuleCat.Presheaf.Monoidal

URI: https://scilib.ai/kg/mathlib#instCommRingCarrierObjOppositeRingCatCompCommRingCatForget₂

English

For every object X in C, the ring structure on (R(obj X)) is a commutative ring.

Русский

Для каждого объекта X в C кольцо на R(X) является коммутативным кольцом.

LaTeX

$$$R(X) \\in \\mathrm{CommRing}$ for all X in C.$$

Lean4

instance (X : Cᵒᵖ) : CommRing ((R ⋙ forget₂ _ RingCat).obj X) :=
  inferInstanceAs (CommRing (R.obj X))

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru