ring — Mathlib

English

If I is a two-sided ideal of a ring R, then the quotient R/I carries a natural ring structure.

Русский

Если I — двусторонний идеал кольца R, то фактор-кольцо R/I обладает естественным кольцом.

LaTeX

$$$I \\text{ двусторонний идеал в }R \\Rightarrow R/I \\text{ является кольцом}$$$

Lean4

instance ring (I : Ideal R) [I.IsTwoSided] : Ring (R ⧸ I) :=
  fast_instance%{
      __ : AddCommGroup (R ⧸ I) := inferInstance
      __ : Ring (Quotient.ringCon I).Quotient := inferInstance }

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