eq_top_iff_one

Mathlib.RingTheory.Ideal.Lattice

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

English

An ideal equals top if and only if 1 belongs to it.

Русский

Идеал равен верхнему тогда, когда в нем содержится 1, и наоборот.

LaTeX

$$$I = \\\\top \\\\Leftrightarrow 1 \\\\in I$$$

Lean4

theorem eq_top_iff_one : I = ⊤ ↔ (1 : α) ∈ I :=
  ⟨by rintro rfl; trivial, fun h => eq_top_of_unit_mem _ _ 1 h (by simp)⟩

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

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

Разделы

Аффилиация

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