zero_ne_one_of_proper

Mathlib.RingTheory.Ideal.Span

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

English

If I ≠ ⊤, then 0 ≠ 1 in α; a proper ideal forces the ring to be nontrivial.

Русский

Если I ≠ ⊤, то 0 ≠ 1 в α; правильный идеал подразумевает не тривиальность кольца.

LaTeX

$$$$ \text{If } I \neq \top, \text{ then } 0 \neq 1. $$$$

Lean4

theorem zero_ne_one_of_proper {I : Ideal α} (h : I ≠ ⊤) : (0 : α) ≠ 1 := fun hz =>
  I.ne_top_iff_one.1 h <| hz ▸ I.zero_mem

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

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

Разделы

Аффилиация

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