instUniqueQuotientTop

Mathlib.RingTheory.Ideal.Quotient.Basic

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

English

The quotient by the top ideal is a unique (has a single element) quotient.

Русский

Фактор по верхнему идеалу единственный (имеет один элемент).

LaTeX

$$$|R / \top| = 1$$$

Lean4

instance : Unique (R ⧸ (⊤ : Ideal R)) :=
  ⟨⟨0⟩, by rintro ⟨x⟩; exact Quotient.eq_zero_iff_mem.mpr Submodule.mem_top⟩

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

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

Разделы

Аффилиация

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