instOne

Mathlib.Algebra.RingQuot

URI: https://scilib.ai/kg/mathlib#RingQuot.instOne

English

In the quotient ring obtained from a semiring by a relation, the multiplicative identity is the image of 1 from the base ring.

Русский

В кольце-остатке, полученном по отношению, единица умножения есть образ единицы из исходного кольца.

LaTeX

$$$1_{\mathrm{Quot}(R,r)} = \overline{1_R}$$$

Lean4

instance : One (RingQuot r) :=
  ⟨one r⟩

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

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

Разделы

Аффилиация

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