commRing

Mathlib.RingTheory.Perfection

URI: https://scilib.ai/kg/mathlib#ModP.commRing

English

ModP O p carries a natural commutative ring structure as a quotient of O by the principal ideal (p).

Русский

ModP O p имеет естественную структуру коммутативного кольца как фактор по идеалу (p).

LaTeX

$$$\text{ModP}(O,p) \text{ is a commutative ring }\; \text{ModP}(O,p) = O / (p).$$$

Lean4

instance commRing : CommRing (ModP O p) :=
  Ideal.Quotient.commRing (Ideal.span {(p : O)} : Ideal O)

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

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

Разделы

Аффилиация

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