isDomain_of_le_nonZeroDivisors — Mathlib

English

If R is a domain and M ⊆ nonZeroDivisors(R), then Localization M is a domain.

Русский

Если R — домен, и M ⊆ nonZeroDivisors(R), то Localization M является доменом.

LaTeX

$$$\\text{IsDomain}(R) \\land (M \\subseteq \\operatorname{nonZeroDivisors}(R)) \\Rightarrow \\text{IsDomain}(\\mathrm{Localization}\\ M)$$$

Lean4

/-- A `CommRing` `S` which is the localization of an integral domain `R` at a subset of
non-zero elements is an integral domain. -/
theorem isDomain_of_le_nonZeroDivisors (hM : M ≤ nonZeroDivisors R) : IsDomain S
    where
  __ : IsCancelMulZero S := (toLocalizationMap M S).isCancelMulZero
  __ : Nontrivial S := (toLocalizationMap M S).nontrivial fun h ↦ zero_notMem_nonZeroDivisors (hM h)

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