bot_prime — Mathlib

English

Under suitable conditions, the bottom ideal is prime.

Русский

При определенных условиях нулевой идеал является простым.

LaTeX

$$⊥ \text{prime in suitable ring}$$

Lean4

theorem bot_prime [Nontrivial α] [NoZeroDivisors α] : (⊥ : Ideal α).IsPrime :=
  ⟨fun h => one_ne_zero (α := α) (by rwa [Ideal.eq_top_iff_one, Submodule.mem_bot] at h), fun h =>
    mul_eq_zero.mp (by simpa only [Submodule.mem_bot] using h)⟩

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