isDomain_iff_prime — Mathlib

English

For a commutative ring and an ideal I, the quotient R/I is a domain if and only if I is prime.

Русский

Для коммутативного кольца и идеала I, фактор-кольцо R/I является доменом тогда и только тогда, когда I является простым.

LaTeX

$$$IsDomain (R/I) \iff I.IsPrime$$$

Lean4

theorem isDomain_iff_prime : IsDomain (R ⧸ I) ↔ I.IsPrime :=
  by
  refine ⟨fun H => ⟨zero_ne_one_iff.1 ?_, fun {x y} h => ?_⟩, fun h => inferInstance⟩
  · haveI : Nontrivial (R ⧸ I) := ⟨H.2.1⟩
    exact zero_ne_one
  · simp only [← eq_zero_iff_mem, (mk I).map_mul] at h ⊢
    haveI := @IsDomain.to_noZeroDivisors (R ⧸ I) _ H
    exact eq_zero_or_eq_zero_of_mul_eq_zero h

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