instIsPrincipalIdealRingLocalizationAlgebraMapSubmonoidPrimeComplOfIsDedekindDomainOfFiniteOfNeZeroIdeal

English

Under Dedekind hypotheses, the localization of a prime-complement algebra is a principal ideal ring.

Русский

При допущениях Dedekind локализация по primeCompl образует кольцо с главными идеалами.

LaTeX

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

Lean4

instance [IsDedekindDomain R] [IsDedekindDomain S] [Module.Finite R S] [hP : NeZero P] : IsPrincipalIdealRing Sₚ :=
  IsDedekindDomain.isPrincipalIdealRing_localization_over_prime S P (fun h ↦ hP.1 h)

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