instOrderBotOfIsDomain — Mathlib

English

In a domain, the prime spectrum has a bottom element, given by the prime corresponding to the zero ideal:

Русский

В домене спектр простых идеалов имеет нижний элемент, соответствующий нулевому идеалу:

LaTeX

$$Если R — домен, то нижний элемент спектра простых идеалов равен примитивному нулю, то есть бот PrimeSpectrum(R) соответствует ⊥.$$

Lean4

instance [IsDomain R] : OrderBot (PrimeSpectrum R)
    where
  bot := ⟨⊥, Ideal.bot_prime⟩
  bot_le I := @bot_le _ _ _ I.asIdeal

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