instIsDedekindDomainLocalizationAlgebraMapSubmonoidPrimeCompl

English

If R and S are Dedekind domains and P is a nonzero prime ideal, then the localization at PĭprimeCompl yields a principal ideal ring.

Русский

Если R и S — Дедекиндовы, и P — неприводимый простой идеал, локализация по primeCompl даёт кольцо с главными идеалами.

LaTeX

$$$\text{IsPrincipalIdealRing} (Localization (Algebra.algebraMapSubmonoid S P.primeCompl))$$$

Lean4

instance [IsDedekindDomain S] : IsDedekindDomain Sₚ :=
  isDedekindDomain S (algebraMapSubmonoid_le_nonZeroDivisors_of_faithfulSMul _ P.primeCompl_le_nonZeroDivisors) _

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