def DedekindDomainEquiv.CondIntegrallyClosed (A : Type u_1) [CommRing A] : Prop

def DedekindDomainEquiv.CondDvrLocalizations (A : Type u_1) [CommRing A] [IsDomain A] : Prop

def DedekindDomainEquiv.CondInvertibleIdeals (A : Type u_1) [CommRing A] [IsDomain A] : Prop

def DedekindDomainEquiv.CondPrimeFactorization (A : Type u_1) [CommRing A] : Prop

def DedekindDomainEquiv.CondContainIsDivide (A : Type u_1) [CommRing A] : Prop

def DedekindDomainEquiv.CondPrincipalProduct (A : Type u_1) [CommRing A] : Prop

def DedekindDomainEquiv.CondQuotientPIR (A : Type u_1) [CommRing A] : Prop

def DedekindDomainEquiv.CondTwoGenerator (A : Type u_1) [CommRing A] : Prop

theorem DedekindDomainEquiv.integrallyClosed_iff_dvrLocalizations (A : Type u_1) [CommRing A] [IsDomain A] : CondIntegrallyClosed A ↔ CondDvrLocalizations A

theorem DedekindDomainEquiv.integrallyClosed_iff_invertibleIdeals (A : Type u_1) [CommRing A] [IsDomain A] : CondIntegrallyClosed A ↔ CondInvertibleIdeals A

theorem DedekindDomainEquiv.integrallyClosed_to_primeFactorization (A : Type u_1) [CommRing A] (h : CondIntegrallyClosed A) : CondPrimeFactorization A

theorem DedekindDomainEquiv.integrallyClosed_to_containIsDivide (A : Type u_1) [CommRing A] [IsDomain A] (h : CondIntegrallyClosed A) : CondContainIsDivide A

theorem DedekindDomainEquiv.primeFactorization_to_integrallyClosed (A : Type u_2) [CommRing A] [IsDomain A] : CondPrimeFactorization A → CondIntegrallyClosed A

theorem DedekindDomainEquiv.containIsDivide_to_integrallyClosed (A : Type u_1) [CommRing A] [IsDomain A] : CondContainIsDivide A → CondIntegrallyClosed A

theorem DedekindDomainEquiv.integrallyClosed_to_principalProduct (A : Type u_1) [CommRing A] [IsDomain A] (h : CondIntegrallyClosed A) : CondPrincipalProduct A

theorem DedekindDomainEquiv.principalProduct_to_integrallyClosed (A : Type u_1) [CommRing A] [IsDomain A] : CondPrincipalProduct A → CondIntegrallyClosed A

theorem DedekindDomainEquiv.integrallyClosed_to_quotientPIR (A : Type u_1) [CommRing A] (h : CondIntegrallyClosed A) : CondQuotientPIR A

theorem DedekindDomainEquiv.quotientPIR_noetherian (A : Type u_1) [CommRing A] [IsDomain A] (h7 : CondQuotientPIR A) : IsNoetherianRing A

theorem DedekindDomainEquiv.quotientPIR_dvr (A : Type u_1) [CommRing A] [IsDomain A] (h7 : CondQuotientPIR A) (P : Ideal A) (hPne : P ≠ ⊥) (hPpr : P.IsPrime) : IsDiscreteValuationRing (Localization.AtPrime P)

theorem DedekindDomainEquiv.quotientPIR_to_integrallyClosed (A : Type u_1) [CommRing A] [IsDomain A] : CondQuotientPIR A → CondIntegrallyClosed A

theorem DedekindDomainEquiv.integrallyClosed_to_twoGenerator (A : Type u_1) [CommRing A] (h : CondIntegrallyClosed A) : CondTwoGenerator A

theorem DedekindDomainEquiv.twoGenerator_to_quotientPIR (A : Type u_1) [CommRing A] (h : CondTwoGenerator A) : CondQuotientPIR A

theorem DedekindDomainEquiv.twoGenerator_to_integrallyClosed (A : Type u_1) [CommRing A] [IsDomain A] : CondTwoGenerator A → CondIntegrallyClosed A

theorem DedekindDomainEquiv.dedekindDomain_tfae (A : Type u_1) [CommRing A] [IsDomain A] : [CondIntegrallyClosed A, CondDvrLocalizations A, CondInvertibleIdeals A, CondPrimeFactorization A, CondContainIsDivide A, CondPrincipalProduct A, CondQuotientPIR A, CondTwoGenerator A].TFAE

theorem FractionalIdealLocalization.localization_comm_add {A : Type u_1} [CommRing A] {K : Type u_2} {K' : Type u_3} [Field K] [Field K'] [Algebra A K] [Algebra A K'] (I J : FractionalIdeal (nonZeroDivisors A) K) (h : K ≃ₐ[A] K') : FractionalIdeal.map (↑h) (I + J) = FractionalIdeal.map (↑h) I + FractionalIdeal.map (↑h) J

theorem FractionalIdealLocalization.localization_comm_mul {A : Type u_1} [CommRing A] {K : Type u_2} {K' : Type u_3} [Field K] [Field K'] [Algebra A K] [Algebra A K'] (I J : FractionalIdeal (nonZeroDivisors A) K) (h : K ≃ₐ[A] K') : FractionalIdeal.map (↑h) (I * J) = FractionalIdeal.map (↑h) I * FractionalIdeal.map (↑h) J

theorem FractionalIdealLocalization.localization_comm_div {A : Type u_1} [CommRing A] [IsDomain A] {K : Type u_2} {K' : Type u_3} [Field K] [Field K'] [Algebra A K] [Algebra A K'] [IsFractionRing A K] [IsFractionRing A K'] (I J : FractionalIdeal (nonZeroDivisors A) K) (h : K ≃ₐ[A] K') : FractionalIdeal.map (↑h) (I / J) = FractionalIdeal.map (↑h) I / FractionalIdeal.map (↑h) J

def FractionalIdealLocalization.localizationRingEquiv {A : Type u_1} [CommRing A] {K : Type u_2} {K' : Type u_3} [Field K] [Field K'] [Algebra A K] [Algebra A K'] (h : K ≃ₐ[A] K') : FractionalIdeal (nonZeroDivisors A) K ≃+* FractionalIdeal (nonZeroDivisors A) K'

noncomputable def FractionalIdealLocalization.fractionFieldEquiv {A : Type u_1} [CommRing A] {K : Type u_2} {K' : Type u_3} [Field K] [Field K'] [Algebra A K] [Algebra A K'] [IsFractionRing A K] [IsFractionRing A K'] : K ≃ₐ[A] K'

theorem FractionalIdealLocalization.nonZeroDivisors_le_comap_localizationAtPrime {A : Type u_1} [CommRing A] [IsDomain A] (p : Ideal A) [p.IsPrime] : nonZeroDivisors A ≤ Submonoid.comap (algebraMap A (Localization.AtPrime p)) (nonZeroDivisors (Localization.AtPrime p))

noncomputable def FractionalIdealLocalization.localizationAtPrimeHom {A : Type u_1} [CommRing A] [IsDomain A] (p : Ideal A) [p.IsPrime] : FractionalIdeal (nonZeroDivisors A) (FractionRing A) →+* FractionalIdeal (nonZeroDivisors (Localization.AtPrime p)) (FractionRing A)

theorem FractionalIdealLocalization.localization_atPrime_add {A : Type u_1} [CommRing A] [IsDomain A] (p : Ideal A) [p.IsPrime] (I J : FractionalIdeal (nonZeroDivisors A) (FractionRing A)) : FractionalIdeal.extended (FractionRing A) ⋯ (I + J) = FractionalIdeal.extended (FractionRing A) ⋯ I + FractionalIdeal.extended (FractionRing A) ⋯ J

theorem FractionalIdealLocalization.localization_atPrime_mul {A : Type u_1} [CommRing A] [IsDomain A] (p : Ideal A) [p.IsPrime] (I J : FractionalIdeal (nonZeroDivisors A) (FractionRing A)) : FractionalIdeal.extended (FractionRing A) ⋯ (I * J) = FractionalIdeal.extended (FractionRing A) ⋯ I * FractionalIdeal.extended (FractionRing A) ⋯ J

theorem FractionalIdealLocalization.localization_map_eq_id {A : Type u_1} [CommRing A] [IsDomain A] (p : Ideal A) [p.IsPrime] : IsLocalization.map (FractionRing A) (algebraMap A (Localization.AtPrime p)) ⋯ = RingHom.id (FractionRing A)