ne_top_iff_one

Mathlib.RingTheory.Ideal.Lattice

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

English

An ideal I is not the whole ring iff 1 ∉ I.

Русский

Идеал I не является вселом кольцом тогда и только тогда, когда 1 ∉ I.

LaTeX

$$$I \\\\neq \\\\top \\\\Leftrightarrow 1 \\\\notin I$$$

Lean4

theorem ne_top_iff_one : I ≠ ⊤ ↔ (1 : α) ∉ I :=
  not_congr I.eq_top_iff_one

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

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

Разделы

Аффилиация

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