one_mem_iff

Mathlib.RingTheory.TwoSidedIdeal.Lattice

URI: https://scilib.ai/kg/mathlib#TwoSidedIdeal.one_mem_iff

← MathLib Explorer

English

For a two-sided ideal I in a ring, 1 ∈ I if and only if I = ⊤ (the whole ring).

Русский

Для идеала I кольца, 1 ∈ I тогда и только тогда, когда I = ⊤.

LaTeX

$$$1 \\in I \\iff I = \\top$$$

Lean4

theorem one_mem_iff {R : Type*} [NonAssocRing R] (I : TwoSidedIdeal R) : (1 : R) ∈ I ↔ I = ⊤ :=
  ⟨fun h => eq_top_iff.2 fun x _ => by simpa using I.mul_mem_left x _ h, fun h ↦ h.symm ▸ trivial⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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