isDomain_localization — Mathlib

English

The localization of an integral domain at a subset of nonzero elements is again an integral domain.

Русский

Локализация интегрального домена по подмножество ненулевых элементов снова является интегральным доменом.

LaTeX

$$$\\text{IsDomain}(R) \\Rightarrow \\text{IsDomain}(\\mathrm{Localization}(M))$$$

Lean4

/-- The localization of an integral domain to a set of non-zero elements is an integral domain. -/
theorem isDomain_localization {M : Submonoid R} (hM : M ≤ nonZeroDivisors R) : IsDomain (Localization M) :=
  isDomain_of_le_nonZeroDivisors _ hM

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