one_quot

Mathlib.Algebra.RingQuot

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

English

The unit in the quotient is the image of one: 1_{Quot} = [1].

Русский

Единица в кольце-остатке — образ единицы: 1_{Quot} = [1].

LaTeX

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

Lean4

theorem one_quot : (⟨Quot.mk _ 1⟩ : RingQuot r) = 1 :=
  show _ = one r by rw [one_def]

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

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

Разделы

Аффилиация

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