class IsSemilocal (A : Type u_1) [CommRing A] : Prop

• finite_maximalIdeals : {𝔪 : Ideal A | 𝔪.IsMaximal}.Finite

theorem Ideal.finite_setOf_isPrime_and_mem {A : Type u_1} [CommRing A] [IsDomain A] [IsDedekindDomain A] (a : A) (ha : a ≠ 0) : {P : Ideal A | P.IsPrime ∧ a ∈ P}.Finite

theorem Ideal.finite_setOf_isPrime_and_le {A : Type u_1} [CommRing A] [IsDedekindDomain A] {I : Ideal A} (hI : I ≠ ⊥) : {p : Ideal A | p.IsPrime ∧ I ≤ p}.Finite

theorem Ideal.count_normalizedFactors_eq_zero_iff {A : Type u_1} [CommRing A] [IsDedekindDomain A] {𝔭 I : Ideal A} (hp : 𝔭.IsPrime) (hI : I ≠ ⊥) : Multiset.count 𝔭 (UniqueFactorizationMonoid.normalizedFactors I) = 0 ↔ ¬I ≤ 𝔭

theorem FractionalIdeal.count_eq_zero_for_all_but_finitely_many {A : Type u_1} [CommRing A] [IsDedekindDomain A] {K : Type u_2} [Field K] [Algebra A K] [IsFractionRing A K] (I : FractionalIdeal (nonZeroDivisors A) K) : I ≠ 0 → {v : IsDedekindDomain.HeightOneSpectrum A | count K v I ≠ 0}.Finite

theorem IsDedekindDomain.isPrincipalIdealRing_of_isSemilocal (R : Type u_3) [CommRing R] [IsDedekindDomain R] [IsSemilocal R] : IsPrincipalIdealRing R

theorem fractionalIdeal_isUnit_iff_isPrincipal (A : Type u_3) [CommRing A] [IsDomain A] [IsLocalRing A] [IsNoetherianRing A] (K : Type u_4) [Field K] [Algebra A K] [IsFractionRing A K] (I : FractionalIdeal (nonZeroDivisors A) K) (hI : I ≠ 0) : IsUnit I ↔ (↑I).IsPrincipal

theorem FractionalIdeal.mul_inv_eq_one_of_ne_zero {A' : Type u_3} [CommRing A'] [IsDomain A'] [IsDedekindDomain A'] {K' : Type u_4} [Field K'] [Algebra A' K'] [IsFractionRing A' K'] (I : FractionalIdeal (nonZeroDivisors A') K') (hI : I ≠ 0) : I * I⁻¹ = 1

theorem isCoprime_span_singleton_of_not_mem_maximal {R : Type u_3} [CommRing R] {P : Ideal R} (hPm : P.IsMaximal) {s : R} (hs : s ∉ P) : IsCoprime (Ideal.span {s}) P

theorem isPrincipalIdealRing_quotient_prime_pow {R : Type u_3} [CommRing R] [IsDomain R] [IsDedekindDomain R] (P : Ideal R) [hPm : P.IsMaximal] (n : ℕ) : IsPrincipalIdealRing (R ⧸ P ^ n)

theorem Ideal.Quotient.isPrincipalIdealRing_of_isDedekindDomain {R : Type u_3} [CommRing R] [IsDomain R] [IsDedekindDomain R] {I : Ideal R} (hI : I ≠ ⊥) : IsPrincipalIdealRing (R ⧸ I)

noncomputable def FractionalIdeal.localizeAtPrime {A : Type u_3} [CommRing A] [IsDomain A] (𝔪 : Ideal A) [𝔪.IsPrime] (I : FractionalIdeal (nonZeroDivisors A) (FractionRing A)) : FractionalIdeal (nonZeroDivisors (Localization.AtPrime 𝔪)) (FractionRing A)

theorem FractionalIdeal.localizeAtPrime_ne_zero {A : Type u_3} [CommRing A] [IsDomain A] (𝔪 : Ideal A) [𝔪.IsPrime] {I : FractionalIdeal (nonZeroDivisors A) (FractionRing A)} (hI : I ≠ 0) : localizeAtPrime 𝔪 I ≠ 0

def FractionalIdeal.IsLocallyPrincipal {A : Type u_3} [CommRing A] [IsDomain A] (I : FractionalIdeal (nonZeroDivisors A) (FractionRing A)) : Prop

theorem FractionalIdeal.isUnit_localizeAtPrime_of_isUnit {A : Type u_3} [CommRing A] [IsDomain A] [IsNoetherianRing A] (I : FractionalIdeal (nonZeroDivisors A) (FractionRing A)) (hI : IsUnit I) (𝔪 : Ideal A) [𝔪.IsMaximal] : IsUnit (localizeAtPrime 𝔪 I)

theorem FractionalIdeal.inv_localizeAtPrime_le {A : Type u_3} [CommRing A] [IsDomain A] [IsNoetherianRing A] (𝔪 : Ideal A) [𝔪.IsPrime] (I : FractionalIdeal (nonZeroDivisors A) (FractionRing A)) : (localizeAtPrime 𝔪 I)⁻¹ ≤ localizeAtPrime 𝔪 I⁻¹

theorem FractionalIdeal.isUnit_iff_isUnit_localizeAtPrime {A : Type u_3} [CommRing A] [IsDomain A] [IsNoetherianRing A] (I : FractionalIdeal (nonZeroDivisors A) (FractionRing A)) : IsUnit I ↔ ∀ (𝔪 : Ideal A) [inst : 𝔪.IsMaximal], IsUnit (localizeAtPrime 𝔪 I)

theorem FractionalIdeal.isUnit_iff_isUnit_localizeAtPrime_all_primes {A : Type u_3} [CommRing A] [IsDomain A] [IsNoetherianRing A] (I : FractionalIdeal (nonZeroDivisors A) (FractionRing A)) : IsUnit I ↔ ∀ (𝔭 : Ideal A) [inst : 𝔭.IsPrime], IsUnit (localizeAtPrime 𝔭 I)

theorem FractionalIdeal.isUnit_iff_isUnit_localize_prime_maximal {A : Type u_3} [CommRing A] [IsDomain A] [IsNoetherianRing A] (I : FractionalIdeal (nonZeroDivisors A) (FractionRing A)) : (IsUnit I ↔ ∀ (𝔪 : Ideal A) [inst : 𝔪.IsMaximal], IsUnit (localizeAtPrime 𝔪 I)) ∧ (IsUnit I ↔ ∀ (𝔭 : Ideal A) [inst : 𝔭.IsPrime], IsUnit (localizeAtPrime 𝔭 I))

theorem FractionalIdeal.isUnit_iff_isLocallyPrincipal {A : Type u_3} [CommRing A] [IsDomain A] [IsNoetherianRing A] (I : FractionalIdeal (nonZeroDivisors A) (FractionRing A)) (hI : I ≠ 0) : IsUnit I ↔ I.IsLocallyPrincipal