instRingQuotient

Mathlib.RingTheory.Ideal.Quotient.Defs

URI: https://scilib.ai/kg/mathlib#Ideal.Quotient.instRingQuotient

English

If R is a commutative ring and I is an ideal, then R/I is a ring.

Русский

Пусть R — коммутативное кольцо, и I — идеал. Тогда R/I является кольцом.

LaTeX

$$$R \\text{ коммутативное кольцо},\\ I \\text{ идеал} \\Rightarrow R/I \\text{ — кольцо}$$$

Lean4

instance {R} [CommRing R] (I : Ideal R) : Ring (R ⧸ I) :=
  fast_instance%inferInstance

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

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

Разделы

Аффилиация

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