def localization_primeIdeal_orderIso {A : Type u_1} [CommRing A] (S : Submonoid A) {B : Type u_2} [CommRing B] [Algebra A B] [IsLocalization S B] : { 𝔮 : Ideal B // 𝔮.IsPrime } ≃o { 𝔭 : Ideal A // 𝔭.IsPrime ∧ Disjoint ↑S ↑𝔭 }

def Submodule.localizedInField {A : Type u_3} [CommRing A] {K : Type u_4} [Field K] [Algebra A K] (M : Submodule A K) (S : Submonoid A) : Submodule A K

theorem submodule_eq_iInf_localizedInField_maximal (A : Type u_1) [CommRing A] [IsDomain A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] (M : Submodule A K) : ⨅ (v : MaximalSpectrum A), M.localizedInField v.asIdeal.primeCompl = M

theorem submodule_eq_iInf_localizedInField_prime (A : Type u_1) [CommRing A] [IsDomain A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] (M : Submodule A K) : ⨅ (v : PrimeSpectrum A), M.localizedInField v.asIdeal.primeCompl = M

theorem submodule_eq_iInf_localizedInField (A : Type u_1) [CommRing A] [IsDomain A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] (M : Submodule A K) : ⨅ (v : MaximalSpectrum A), M.localizedInField v.asIdeal.primeCompl = M ∧ ⨅ (v : PrimeSpectrum A), M.localizedInField v.asIdeal.primeCompl = M

theorem subalgebra_iInf_localization_maximal_eq_bot (A : Type u_1) [CommRing A] [IsDomain A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] : ⨅ (v : MaximalSpectrum A), Localization.subalgebra.ofField K v.asIdeal.primeCompl ⋯ = ⊥

theorem ideal_eq_iInf_comap_map_localization_maximal (A : Type u_1) [CommRing A] [IsDomain A] (I : Ideal A) : ⨅ (𝔪 : MaximalSpectrum A), Ideal.comap (algebraMap A (Localization 𝔪.asIdeal.primeCompl)) (Ideal.map (algebraMap A (Localization 𝔪.asIdeal.primeCompl)) I) = I

theorem ideal_eq_iInf_comap_map_localization_prime (A : Type u_1) [CommRing A] [IsDomain A] (I : Ideal A) : ⨅ (𝔭 : PrimeSpectrum A), Ideal.comap (algebraMap A (Localization 𝔭.asIdeal.primeCompl)) (Ideal.map (algebraMap A (Localization 𝔭.asIdeal.primeCompl)) I) = I

theorem ideal_eq_iInf_comap_map_localization (A : Type u_1) [CommRing A] [IsDomain A] (I : Ideal A) : ⨅ (𝔪 : MaximalSpectrum A), Ideal.comap (algebraMap A (Localization 𝔪.asIdeal.primeCompl)) (Ideal.map (algebraMap A (Localization 𝔪.asIdeal.primeCompl)) I) = ⨅ (𝔭 : PrimeSpectrum A), Ideal.comap (algebraMap A (Localization 𝔭.asIdeal.primeCompl)) (Ideal.map (algebraMap A (Localization 𝔭.asIdeal.primeCompl)) I) ∧ ⨅ (𝔪 : MaximalSpectrum A), Ideal.comap (algebraMap A (Localization 𝔪.asIdeal.primeCompl)) (Ideal.map (algebraMap A (Localization 𝔪.asIdeal.primeCompl)) I) = I

theorem isDVR_localization_iff_integrallyClosed_dimensionLEOne (A : Type u_1) [CommRing A] [IsDomain A] [IsNoetherianRing A] : (∀ (P : Ideal A), P ≠ ⊥ → ∀ (x : P.IsPrime), IsDiscreteValuationRing (Localization.AtPrime P)) ↔ IsIntegrallyClosed A ∧ Ring.DimensionLEOne A

theorem integrallyClosed_dimensionLEOne_iff_isDedekindDomain (A : Type u_1) [CommRing A] [IsDomain A] [IsNoetherianRing A] : IsIntegrallyClosed A ∧ Ring.DimensionLEOne A ↔ IsDedekindDomain A

theorem pid_isDedekindDomain (R : Type u_1) [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] : IsDedekindDomain R

instance Int.isDedekindDomain : IsDedekindDomain ℤ

instance Polynomial.isDedekindDomain (k : Type u_1) [Field k] : IsDedekindDomain (Polynomial k)