eq_bot_of_prime

Mathlib.RingTheory.Ideal.Prime

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

English

In a division semiring, any prime ideal I is the bottom ideal.

Русский

В делительном полугольнике любой простой идеал I равен нулю.

LaTeX

$$I.IsPrime \Rightarrow I = \perp$$

Lean4

theorem eq_bot_of_prime [h : I.IsPrime] : I = ⊥ :=
  or_iff_not_imp_right.mp I.eq_bot_or_top h.1

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

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

Разделы

Аффилиация

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