noZeroDivisors — Mathlib

English

If I is a prime ideal in a commutative ring, then the quotient R/I is a domain; conversely, if R/I is a domain, I is prime.

Русский

Если I — простой идеал в коммутативном кольце, то R/I — интегральное доменное кольцо; наоборот, если R/I — домен, то I — простой.

LaTeX

$$IsDomain (R ⧸ I) ⇔ I.IsPrime$$

Lean4

instance noZeroDivisors [hI : I.IsPrime] : NoZeroDivisors (R ⧸ I) where
  eq_zero_or_eq_zero_of_mul_eq_zero
    {a
      b} :=
    Quotient.inductionOn₂' a b fun {_ _} hab =>
      (hI.mem_or_mem (eq_zero_iff_mem.1 hab)).elim (Or.inl ∘ eq_zero_iff_mem.2) (Or.inr ∘ eq_zero_iff_mem.2)

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