isDomain_of_local_atPrime — Mathlib

English

The localization at the complement of a prime ideal is an integral domain when the original ring is an integral domain.

Русский

Локализация по дополнению к простому идеалу является целочисленным доменом, если исходное кольцо — домен.

LaTeX

$$$$ \text{IsDomain}(\operatorname{Localization.AtPrime} P) $$$$

Lean4

/-- The localization of an integral domain at the complement of a prime ideal is an integral domain.
-/
instance isDomain_of_local_atPrime {P : Ideal A} (_ : P.IsPrime) : IsDomain (Localization.AtPrime P) :=
  isDomain_localization P.primeCompl_le_nonZeroDivisors

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