mem_of_one_mem

Mathlib.RingTheory.Ideal.GoingUp

URI: https://scilib.ai/kg/mathlib#Ideal.mem_of_one_mem

English

If 1 belongs to an ideal I of S, then I is the whole ring, i.e., I = S.

Русский

Если единица принадлежит идеалу I, то I равен всему кольцу.

LaTeX

$$$$1 \in I \Rightarrow I = S.$$$$

Lean4

theorem mem_of_one_mem (h : (1 : S) ∈ I) (x) : x ∈ I :=
  (I.eq_top_iff_one.mpr h).symm ▸ mem_top

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

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

Разделы

Аффилиация

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