of_bot_isPrime — Mathlib

English

If the bottom ideal of a ring is prime, then the ring is a domain (no zero divisors).

Русский

Если нулевой идеал кольца прост, то кольцо является доменом (нет нулевых делителей).

LaTeX

$$\text{If } (0) \text{ is prime, then no zero divisors exist: } \forall a,b, ab=0 \Rightarrow a=0 \lor b=0$$

Lean4

theorem of_bot_isPrime (A : Type*) [Ring A] [hbp : (⊥ : Ideal A).IsPrime] : IsDomain A :=
  @NoZeroDivisors.to_isDomain A _ ⟨1, 0, fun h => hbp.one_notMem h⟩ ⟨fun h => hbp.2 h⟩

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