primesOver_bot — Mathlib

English

Under the given hypotheses, primesOver of the bottom ideal equals the bottom ideal, i.e., there are no nontrivial primes lying over ⊥.

Русский

При заданных гипотезах primesOver(⊥) = {⊥}, то есть не существует ненулевых примитивных примы над ⊥.

LaTeX

$$$\text{primesOver}(\bot) = \{\bot\}$$$

Lean4

theorem primesOver_bot [Nontrivial A] [IsDomain B] : primesOver (⊥ : Ideal A) B = {⊥} :=
  by
  ext p
  refine ⟨fun ⟨_, ⟨h⟩⟩ ↦ p.eq_bot_of_comap_eq_bot h.symm, ?_⟩
  rintro rfl
  exact ⟨Ideal.bot_prime, Ideal.bot_liesOver_bot A B⟩

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