instNonemptyQuotient

Mathlib.RingTheory.Ideal.Quotient.Defs

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

English

The quotient ring R/I is nonempty (for instance, the coset of any element).

Русский

Фактор-кольцо R/I непусто (например, косета любого элемента).

LaTeX

$$$R/I \\neq \\emptyset$$$

Lean4

instance : Nonempty (R ⧸ I) :=
  ⟨mk I 37⟩

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

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

Разделы

Аффилиация

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