theorem isValuationSubring_iff_forall_units {K : Type u_1} [Field K] (R : Subring K) : (∀ (x : K), x ∈ R ∨ x⁻¹ ∈ R) ↔ ∀ (x : K), x ≠ 0 → x ∈ R ∨ x⁻¹ ∈ R

def ValuationSubring.ofSubring_units {K : Type u_1} [Field K] (R : Subring K) (hR : ∀ (x : K), x ≠ 0 → x ∈ R ∨ x⁻¹ ∈ R) : ValuationSubring K

theorem valuationRing_isLocal (R : Type u_1) [CommRing R] [IsDomain R] [ValuationRing R] : IsLocalRing R

theorem ValuationRing.ideal_le_or_le {R : Type u_1} [CommRing R] [IsDomain R] [ValuationRing R] (𝔞 𝔟 : Ideal R) : 𝔞 ≤ 𝔟 ∨ 𝔟 ≤ 𝔞

theorem ValuationRing.fg_isPrincipal {R : Type u_1} [CommRing R] [IsDomain R] [ValuationRing R] (I : Ideal R) (hI : I.FG) : Submodule.IsPrincipal I

theorem valuationRing_iff_of_localRing (R : Type u_1) [CommRing R] [IsDomain R] [IsLocalRing R] : ValuationRing R ∧ ¬IsField R ↔ ¬IsField R ∧ IsBezout R

theorem localRing_iff_unique_maximal_ideal (R : Type u_1) [CommSemiring R] : IsLocalRing R ↔ ∃! I : Ideal R, I.IsMaximal

theorem isLocalRing_iff_nonunits_isIdeal (R : Type u_1) [CommRing R] : IsLocalRing R ↔ ∃ (I : Ideal R), ↑I = nonunits R

theorem regularLocalRing_dim_one_iff_dvr (R : Type u_1) [CommRing R] [IsDomain R] : IsRegularLocalRing R ∧ ringKrullDim R = 1 ↔ IsDiscreteValuationRing R

theorem valuationRing_noetherian_iff_dvr (R : Type u_1) [CommRing R] [IsDomain R] (hR : ¬IsField R) : ValuationRing R ∧ IsNoetherianRing R ↔ IsDiscreteValuationRing R

def localizationAtPrime (R : Type u_1) [CommRing R] (𝔭 : Ideal R) [𝔭.IsPrime] : Type u_1

instance localizationAtPrime.isLocalRing (R : Type u_1) [CommRing R] (𝔭 : Ideal R) [𝔭.IsPrime] : IsLocalRing (Localization.AtPrime 𝔭)

theorem localizationAtPrime.maximalIdeal_eq (R : Type u_1) [CommRing R] (𝔭 : Ideal R) [𝔭.IsPrime] : IsLocalRing.maximalIdeal (Localization.AtPrime 𝔭) = Ideal.map (algebraMap R (Localization.AtPrime 𝔭)) 𝔭

noncomputable def valuationOfValuationRing {R : Type u_1} [CommRing R] [IsDomain R] [ValuationRing R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] : Valuation K (ValuationRing.ValueGroup R K)

theorem valuation_mul {R : Type u_1} [CommRing R] [IsDomain R] [ValuationRing R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (x y : K) : (ValuationRing.valuation R K) (x * y) = (ValuationRing.valuation R K) x * (ValuationRing.valuation R K) y

noncomputable def valuationRingEquivInteger {R : Type u_1} [CommRing R] [IsDomain R] [ValuationRing R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] : R ≃+* ↥(ValuationRing.valuation R K).integer

def maximalIdealAtPoint {R : Type u_1} [CommRing R] {k : Type u_2} [Field k] (φ : R →+* k) : Ideal R

theorem maximalIdealAtPoint_isMaximal {R : Type u_1} [CommRing R] {k : Type u_2} [Field k] (φ : R →+* k) (hφ : Function.Surjective ⇑φ) : (maximalIdealAtPoint φ).IsMaximal

@[reducible, inline]

abbrev localRingAtPoint {R : Type u_1} [CommRing R] {k : Type u_2} [Field k] (φ : R →+* k) [(maximalIdealAtPoint φ).IsPrime] : Type u_1

instance localRingAtPoint_isLocalRing {R : Type u_1} [CommRing R] {k : Type u_2} [Field k] (φ : R →+* k) [(maximalIdealAtPoint φ).IsPrime] : IsLocalRing (localRingAtPoint φ)

noncomputable def quotient_maximalIdealAtPoint_ringEquiv {R : Type u_1} [CommRing R] {k : Type u_2} [Field k] (φ : R →+* k) (hφ : Function.Surjective ⇑φ) : R ⧸ maximalIdealAtPoint φ ≃+* k

def localRingAtPoint_algebraMap {R : Type u_1} [CommRing R] {k : Type u_2} [Field k] (φ : R →+* k) [(maximalIdealAtPoint φ).IsPrime] : R →+* localRingAtPoint φ