Chapter 4. Valuation rings
FC13 — Matsumura, Commutative Ring Theory.
This chapter contains 15 definitions, 21 theorems, 2 lemmas, 4 corollaries, 1 example, 1 counterexample, 2 constructions and 1 remark.
Of the 47 statements checked against Lean, 17 are formalized somewhere and 30 are not.
| Status | Statements | Share | What it means |
|---|---|---|---|
| not formalized | 30 | 64% | A documented search found no Lean statement of it anywhere. |
| in Mathlib | 17 | 36% | Mathlib states and proves it. |
| checked in total | 47 |
- Canonical source block: FC13 Matsumura Chapter 4,
FC13-C04-U001–FC13-C04-U047, §§10–12, in canonical source-ID order from Foundational corpus units FC13 Matsumura. The generator retrieves the promoted catalogue throughagent-memory, asserts all 47 IDs occur once and in order, and emits one route per unit. - Project-first inspection used
A=3b2239e161592472b34e02ad3b7da308f9ce7280(Lean 4.33.0, Apache-2.0). The project has category wrappersValuationRingCat,DiscreteValuationRingCat, andDedekindDomainCat, plus fractional-ideal convenience definitions, but these are wrappers around pinned Mathlib and do not own a complete C04 row more fully than P. No row is classifiedproject-existingfrom a wrapper alone. - Pinned Mathlib is
P=db584cd6d46c92f209a44c0f1c829460d327499d, Apache-2.0, Lean 4.33.0. Every promotedmathlibpath/token is validated against that exact checkout. Relevant native areas are valuation subrings/local-subring domination, intrinsic value groups, DVR TFAEs and adic valuations, fractional ideals, and Dedekind ideal factorization. - Current Mathlib was refreshed 2026-09-07 to
H=e281a66114fe17935e6ea7917a01b714d0c1e493, Apache-2.0, Lean 4.34.0-rc2. Current/open searches found no post-pin Krull-ring development closing any §12 unit, and no Krull-Akizuki theorem or Zariski-Riemann valuation-space topology. - Search channels used project source, P, H/current/open Mathlib, Mathlib docs/source, Loogle/LeanSearch-oriented repository tooling, Reservoir/indexed discovery, and GitHub-wide Lean-code search. The only concrete external Krull-domain hit was
acmepjz/lean-iwasawa@7fffeb8c80fbe13f989f318c23cbb0dcf2230092; its relevantIsKrullDomaintheorem development contains explicitsorrys and its predicate uses the canonical height-one localization family rather than Matsumura’s general defining-family object, so it is not a validreference-portor package route. - Strict bundle semantics were enforced. U002 is not credited from the prime/coarsening correspondence without the quotient/composite clauses; U014–U015 are not credited from Mathlib’s multiples-based
Archimedeanpredicate without a checked Hölder embedding theorem; U026–U029 remain unmatched when only constituent projective/localization/height facts exist; and U035 is promoted only because both the integral-closure Dedekind theorem and finiteness of primes over a maximal ideal are explicit at P. - Matsumura’s DVR definition (U019) is value-group based. P defines
IsDiscreteValuationRingby the equivalent local-PID/nonfield condition and proves the associated valuation has value group ℤ, but no checked converse starts from the source value-group definition. U019 is therefore deliberately unmatched, while U020/U021/U024 use the exact pinned DVR valuation and equivalence theorems under their stated hypotheses. - §12 U036–U047 is kept separate from Dedekind/height-one infrastructure: without a completed compatible Krull-ring object, generic DVR localization and factorization results are adjacent evidence only, not source-unit matches.
- Route totals for C04:
mathlib17,project-existing0,package-import0,reference-port0,unmatched30.
Definition: valuation ring
A domain R with fraction field K is a valuation ring if for every x∈K, x∈R or x⁻¹∈R. Its ideals are totally ordered by inclusion, so R is local; the field itself is the trivial valuation ring.
Formalized. Mathlib/RingTheory/Valuation/ValuationRing.lean::ValuationRing, iff_ideal_total, isInteger_or_isInteger, isLocalRing — Mathlib’s valuation-ring class is equivalent to total divisibility/total ordering of ideals; in a fraction field every x or x⁻¹ is integral over the ring interface, and valuation rings are local. A field carries the trivial valuation-ring instance.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Theorem: Theorem 10.1
If R⊊R′⊆K are valuation rings with maximal ideals m,p, then p⊂m⊂R⊂R′ and p≠m; p is prime in R and R′=R_p; R/p is a valuation ring of Frac(R′/p); and inverse images of valuation subrings of R′/p give valuation rings of K contained in R′.
Not formalized. Pinned Mathlib classifies valuation-subring coarsenings by prime ideals (ValuationSubring.primeSpectrumOrderEquiv) and realizes the overring as localization, but no checked declaration packages the quotient valuation ring and inverse-image/composite clauses of Matsumura 10.1 in one exact bundle.
Definition: composite of valuation rings
The inverse-image construction in Theorem 10.1(iv) is the composite valuation ring; every valuation ring of K contained in R′ arises as such a composite.
Not formalized. The inverse-image ingredients and coarsening order are present, but no pinned/current/open/external declaration defines Matsumura’s composite valuation ring and proves that every contained valuation ring arises that way.
Definition: domination of local rings
For local rings R⊇S, R dominates S if m_R∩S=m_S.
Formalized. Mathlib/RingTheory/LocalRing/LocalSubring.lean::LocalSubring, le_def — LocalSubring is ordered precisely by inclusion together with IsLocalHom; the file documents this as domination, equivalently contraction of the dominating maximal ideal to the dominated maximal ideal.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Theorem: Theorem 10.2
For a field K, subring A⊆K and p∈Spec A, there exists a valuation ring R of K containing A whose centre on A is p, i.e. m_R∩A=p.
Formalized. Mathlib/RingTheory/LocalRing/LocalSubring.lean::LocalSubring.ofPrime; Mathlib/RingTheory/Valuation/LocalSubring.lean::LocalSubring.exists_le_valuationSubring — Localizing A at p gives a local subring with center p, and every local subring of a field is dominated by a valuation subring. Its maximal ideal therefore contracts to p, exactly Matsumura 10.2.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Theorem: Theorem 10.3
Every valuation ring is integrally closed.
Formalized. Mathlib/RingTheory/Valuation/LocalSubring.lean::IsIntegrallyClosed — Every valuation subring of a field has an IsIntegrallyClosed instance; transporting along the fraction-field embedding gives the source theorem for valuation rings.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Theorem: Theorem 10.4
The integral closure of A in a field K is the intersection of all valuation rings of K containing A.
Formalized. Mathlib/RingTheory/Valuation/LocalSubring.lean::Subring.eq_iInf_of_isIntegrallyClosedIn — The pinned theorem states that an integrally closed subring of a field is exactly the infimum/intersection of all valuation subrings containing it. Applied to the integral closure of A in K, this is Matsumura 10.4.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Definition: centre and Zariski space of valuations
A valuation ring R of K containing A has centre m_R∩A on A. Zar(K,A) is the set of such valuation rings, called the Zariski space or Zariski Riemann surface of K over A.
Not formalized. Valuation subrings and centers are formalized, but no checked declaration packages the set Zar(K,A) of valuation overrings with center map as a named source-shaped object.
Construction: Zariski topology on Zar(K,A)
For x₁,…,x_n∈K, U(x₁,…,x_n)=Zar(K,A[x₁,…,x_n]); these sets form a basis for the Zariski topology on Zar(K,A).
Not formalized. No pinned/current/open/external Lean declaration defines the basis U(x₁,…,xₙ)=Zar(K,A[x₁,…,xₙ]) on the valuation space.
Theorem: Theorem 10.5
Zar(K,A) is quasi-compact in its Zariski topology.
Not formalized. Because the source valuation-space topology is absent, no checked theorem proves Matsumura 10.5 quasi-compactness.
Definition: ordered abelian group
An abelian group H with a total order is ordered when translation preserves the order; adjoin ∞ larger than every element, with ∞+a=∞.
Formalized. Mathlib/Algebra/Order/Group/Defs.lean::AddCommGroup, IsOrderedAddMonoid; Mathlib/Algebra/Order/Monoid/Unbundled/WithTop.lean::WithTop — Mathlib separates the additive commutative group, linear order, and translation-invariance typeclasses; WithTop adjoins the absorbing top element ∞ with the expected ordered-additive operations.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Definition: additive valuation and value group
An additive valuation v:K→H∪{∞} satisfies v(xy)=v(x)+v(y), v(x+y)≥min(v(x),v(y)), and v(x)=∞ iff x=0. The image of K* is its value group.
Formalized. Mathlib/RingTheory/Valuation/Basic.lean::AddValuation, ValueGroup, ValueGroup₀ — AddValuation is the additive presentation of valuations with top, using min for the ultrametric inequality. ValueGroup/ValueGroup₀ restrict a valuation to the subgroup generated by its nonzero image, exactly the intrinsic value-group construction.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Construction: valuation ring attached to an additive valuation
For v, R_v={x | v(x)≥0} is a valuation ring and m_v={x | v(x)>0} its maximal ideal. Conversely every valuation ring yields such a valuation with value group K/R; valuations with the same valuation ring differ by an order-isomorphism of value groups.
Formalized. Mathlib/RingTheory/Valuation/ValuationSubring.lean::ValuationSubring.valuation, integer_valuation, isEquiv_iff_valuationSubring; Mathlib/RingTheory/Valuation/Basic.lean::Valuation.IsEquiv.orderMonoidIso — A valuation subring has a canonical valuation whose integer ring is exactly the subring; equal valuation subrings are equivalent valuations, and equivalent valuations induce an ordered isomorphism of their intrinsic value groups.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Definition: Archimedean ordered group
An ordered group is Archimedean if it is order-isomorphic to a subgroup of the additive real numbers.
Not formalized. Mathlib has an Archimedean typeclass using the multiples/cofinality condition, but no checked theorem identifies an arbitrary linearly ordered abelian group satisfying it with a subgroup of (ℝ,+) as Matsumura uses for the definition.
Theorem: Theorem 10.6
An ordered group G is Archimedean iff for all a>0 and b∈G there exists n∈N with na>b.
Not formalized. Archimedean/exists_lt_nsmul formalize the right-hand multiples condition, but without the Hölder embedding theorem of U014 there is no checked iff with Matsumura’s subgroup-of-ℝ definition.
Definition: rank and rational rank of an ordered group
A nonzero ordered group has rank one if it is order-isomorphic to a subgroup of R. Its rational rank is the maximal number of elements linearly independent over Z after such an embedding.
Not formalized. Valuation rank-one classes exist, but no compatible declaration defines Matsumura’s ordered-group rank together with rational rank as ℤ-linear rank after an embedding in ℝ.
Example: rank one need not rational rank one
Z+Z√2⊂R has ordered-group rank one and rational rank two.
Not formalized. No checked declaration owns the ordered subgroup ℤ+ℤ√2 ⊂ ℝ with the source rank and rational-rank computations.
Theorem: Theorem 10.7
For a valuation ring R with value group G, G has rank one iff R has Krull dimension one.
Not formalized. Pinned Mathlib has valuation RankOne and Krull dimension separately but no theorem identifying rank one of a valuation ring’s value group with ring Krull dimension one. Current/open/external searches were negative.
Definition: discrete valuation ring
A valuation ring whose value group is isomorphic to Z is a discrete valuation ring (DVR).
Not formalized. Mathlib defines IsDiscreteValuationRing as a local PID that is not a field and proves its associated valuation is rank-one discrete with value group order-isomorphic to ℤ. No checked converse starts from Matsumura’s valuation-ring/value-group-ℤ definition, so the source definition is not directly represented.
Definition: normalised valuation of a DVR
For a DVR R, the additive valuation with value group Z is its normalised additive valuation.
Formalized. Mathlib/RingTheory/Valuation/Discrete/IsDiscreteValuationRing.lean::IsDiscreteValuationRing.isRankOneDiscrete, IsDiscreteValuationRing.maximalIdeal; Mathlib/RingTheory/Valuation/Discrete/RankOne.lean::valueGroup₀_equiv_withZeroMulInt; Mathlib/RingTheory/DedekindDomain/AdicValuation.lean::intValuation, valuation — A DVR’s maximal ideal gives a discrete rank-one valuation; its intrinsic value group is canonically order-isomorphic to integers (with zero added), and the adic/int valuation realizes the normalized integer exponent convention.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Theorem: Theorem 11.1
For a valuation ring R, the following are equivalent: R is a DVR; R is a PID; R is Noetherian. In a DVR every nonzero ideal is a power of the maximal ideal.
Formalized. Mathlib/RingTheory/DiscreteValuationRing/TFAE.lean::IsDiscreteValuationRing.TFAE, tfae_of_isNoetherianRing_of_isLocalRing_of_isDomain; Mathlib/RingTheory/DiscreteValuationRing/Basic.lean::ideal_eq_span_pow_irreducible — Pinned TFAE theorems identify the nonfield local PID/DVR and Noetherian valuation-domain presentations; the DVR ideal theorem writes every nonzero ideal as a power of the maximal/uniformizer ideal.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Definition: uniformising element
If (R,m) is a DVR, t∈R with m=tR is a uniformising element.
Formalized. Mathlib/RingTheory/DiscreteValuationRing/Basic.lean::irreducible_iff_uniformizer, exists_irreducible — In a DVR an irreducible element generates the maximal ideal exactly when it is a uniformizer; existence is explicit.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Counterexample: principal maximal ideal does not characterize DVRs among valuation rings
A composite rank-two valuation ring can have principal maximal ideal while failing to be a DVR; the source constructs one with value group Z² in lexicographic order.
Not formalized. No checked declaration constructs Matsumura’s lexicographically ordered rank-two valuation ring with principal maximal ideal but non-DVR value group.
Theorem: Theorem 11.2
For a ring R the following are equivalent: R is a DVR; R is a local PID and not a field; R is Noetherian local of positive dimension with principal maximal ideal; R is a one-dimensional normal Noetherian local ring.
Formalized. Mathlib/RingTheory/DiscreteValuationRing/TFAE.lean::IsDiscreteValuationRing.TFAE, tfae_of_isNoetherianRing_of_isLocalRing_of_isDomain — The pinned TFAE package compares DVR, local PID nonfield, principal maximal ideal in a Noetherian local domain, integrally closed one-dimensional local domain, and related equivalent criteria, matching Matsumura 11.2.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Definition: fractional and invertible ideals
For a domain R with fraction field K, a fractional ideal is a nonzero R-submodule I⊆K with aI⊆R for some nonzero a∈R. Put I⁻¹={α∈K | αI⊆R}; I is invertible if I⁻¹I=R.
Formalized. Mathlib/RingTheory/FractionalIdeal/Basic.lean::FractionalIdeal; Mathlib/RingTheory/FractionalIdeal/Inverse.lean::inv, mul_inv_cancel_iff — FractionalIdeal is the denominator-bounded submodule of a fraction field; the inverse fractional ideal is defined by the multiplier condition and mul_inv_cancel_iff is exactly invertibility.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Theorem: Theorem 11.3
For a fractional ideal I of a domain R, the following are equivalent: I is invertible; I is projective as an R-module; I is finitely generated and I_P is principal for every maximal ideal P.
Not formalized. Pinned Mathlib proves invertible fractional ideals are finitely generated and has generic projective/localization infrastructure, but no checked declaration packages the three-way equivalence in Matsumura 11.3. Current/open/external search found no exact owner.
Theorem: Theorem 11.4
If R is a Noetherian domain and P≠0 is prime and invertible, then ht P=1 and R_P is a DVR.
Not formalized. Krull height and localization/DVR APIs provide ingredients, but no checked theorem takes a nonzero invertible prime in an arbitrary Noetherian domain and proves both height one and DVR localization as Matsumura 11.4.
Theorem: Theorem 11.5
For a normal Noetherian domain R, every prime divisor of a nonzero principal ideal has height one, and R=⋂_{ht p=1}R_p inside its fraction field.
Not formalized. Pinned Mathlib proves height-one consequences for principal ideals and local integrally-closed criteria, but no declaration states the full theorem that principal prime divisors have height one and the ring is the intersection of all height-one localizations inside its fraction field.
Corollary: normality criterion in codimension one
A Noetherian domain R is normal iff every height-one localisation R_P is a DVR and every prime divisor of a nonzero principal ideal has height one.
Not formalized. The local integrally-closed API and DVR characterizations are present, but no checked declaration proves the complete iff of Matsumura’s codimension-one criterion under exactly the source hypotheses.
Definition: Dedekind ring
A Dedekind ring is a domain in which every nonzero ideal is invertible.
Formalized. Mathlib/RingTheory/DedekindDomain/Ideal/Basic.lean::isDedekindDomain_iff_mul_inv_cancel — For a domain, the pinned iff says IsDedekindDomain exactly when every nonzero fractional ideal multiplies with its inverse to one; restricting to integral ideals is Matsumura’s definition.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Theorem: Theorem 11.6
For a domain R the following are equivalent: R is Dedekind; R is a field or a one-dimensional Noetherian normal domain; every nonzero ideal is a finite product of prime ideals. Such prime-ideal factorisations are unique.
Formalized. Mathlib/RingTheory/DedekindDomain/Basic.lean::isDedekindDomain_iff; Mathlib/RingTheory/DedekindDomain/Ideal/Lemmas.lean::prod_normalizedFactors_eq_self; Mathlib/RingTheory/DedekindDomain/Factorization.lean::Ideal.finprod_heightOneSpectrum_factorization — isDedekindDomain_iff is the Noetherian, integrally closed, dimension≤1 characterization; the factorization APIs give finite prime-ideal factorization with multiplicities and the UFM normalization gives uniqueness.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Definition: rank of a module over a domain
For a domain A with fraction field K, rank_A M is the maximal size of an A-linearly independent subset of M, equivalently dim_K(M⊗_A K).
Formalized. Mathlib/LinearAlgebra/Dimension/Localization.lean::IsFractionRing.rank_right_eq, IsLocalization.rank_eq; Mathlib/LinearAlgebra/Dimension/Basic.lean::Module.rank — Module rank is the cardinal dimension/maximum linear-independence size, and localization/fraction-ring rank is unchanged by extension to the fraction field, giving the source equivalence with the vector-space dimension after tensoring.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Lemma: Krull-Akizuki length bound
If A is one-dimensional Noetherian with fraction field K and M is torsion-free of finite rank r, then for every nonzero a∈A, length(M/aM)≤r·length(A/aA).
Not formalized. Targeted pinned/current/open/external searches found no Lean theorem proving the one-dimensional Noetherian torsion-free finite-rank length inequality.
Theorem: Theorem 11.7 (Krull-Akizuki)
If A is a one-dimensional Noetherian domain with fraction field K, L/K finite algebraic, and A⊆B⊆L, then B is Noetherian of dimension at most one; for every nonzero ideal J⊲B, B/J has finite length as an A-module.
Not formalized. No checked compatible declaration proves that every intermediate ring in a finite algebraic extension of a one-dimensional Noetherian domain is Noetherian of dimension≤1 together with the finite-length quotient assertion.
Corollary: integral closures in finite extensions are Dedekind
If A is a one-dimensional Noetherian domain, L is a finite algebraic extension of its fraction field, and B is the integral closure of A in L, then B is Dedekind and only finitely many primes of B lie over any maximal ideal of A.
Formalized. Mathlib/RingTheory/DedekindDomain/IntegralClosure.lean::integralClosure.isDedekindDomain; Mathlib/RingTheory/DedekindDomain/Ideal/Lemmas.lean::primesOver_finite — For a Dedekind base and finite field extension, the integral closure is Dedekind; one-dimensional Noetherian normality of the source is the preceding characterization, and primesOver_finite gives finiteness over each maximal prime.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Definition: Krull ring and defining family
A domain A with fraction field K is Krull if A is an intersection of DVRs R_lambda of K and, for each nonzero x in K, only finitely many corresponding normalised valuations are nonzero. Such a family is a defining family.
Not formalized. Pinned/current Mathlib contains no Krull-ring/domain predicate matching Matsumura §12. GitHub-wide search found an experimental IsKrullDomain in acmepjz/lean-iwasawa, but the relevant theorem development is explicitly sorry-backed and its definition does not include Matsumura’s general defining-family object; it is not credited as a route. No other complete compatible external owner was found.
Corollary: complete integral closure and subfield stability
Krull rings are completely integrally closed; intersecting a Krull ring with a subfield of its fraction field again gives a Krull ring.
Not formalized. Pinned/current Mathlib contains no Krull-ring/domain predicate matching Matsumura §12. GitHub-wide search found an experimental IsKrullDomain in acmepjz/lean-iwasawa, but the relevant theorem development is explicitly sorry-backed and its definition does not include Matsumura’s general defining-family object; it is not credited as a route. No other complete compatible external owner was found.
Theorem: Theorem 12.1
A localisation of a Krull ring is Krull; a defining family localises by retaining exactly the DVRs containing the localisation.
Not formalized. Pinned/current Mathlib contains no Krull-ring/domain predicate matching Matsumura §12. GitHub-wide search found an experimental IsKrullDomain in acmepjz/lean-iwasawa, but the relevant theorem development is explicitly sorry-backed and its definition does not include Matsumura’s general defining-family object; it is not credited as a route. No other complete compatible external owner was found.
Lemma: Lemma 1 (Nagata)
For finitely many valuation rings R_i of K and an element a in K, one can choose s at least two so that both the inverse of 1+a+…+a^(s-1) and a times that inverse belong to every R_i.
Not formalized. Pinned/current Mathlib contains no Krull-ring/domain predicate matching Matsumura §12. GitHub-wide search found an experimental IsKrullDomain in acmepjz/lean-iwasawa, but the relevant theorem development is explicitly sorry-backed and its definition does not include Matsumura’s general defining-family object; it is not credited as a route. No other complete compatible external owner was found.
Theorem: Theorem 12.2
The intersection of finitely many pairwise noncontained valuation rings is semilocal with those valuation rings as its localisations at the corresponding maximal ideals; if all are DVRs, the intersection is a PID.
Not formalized. Pinned/current Mathlib contains no Krull-ring/domain predicate matching Matsumura §12. GitHub-wide search found an experimental IsKrullDomain in acmepjz/lean-iwasawa, but the relevant theorem development is explicitly sorry-backed and its definition does not include Matsumura’s general defining-family object; it is not credited as a route. No other complete compatible external owner was found.
Theorem: Theorem 12.3
For a Krull ring A, every height-one localisation A_p occurs in every defining family. The family of all A_p with ht p=1 is itself a defining family and is the unique minimal defining family.
Not formalized. Pinned/current Mathlib contains no Krull-ring/domain predicate matching Matsumura §12. GitHub-wide search found an experimental IsKrullDomain in acmepjz/lean-iwasawa, but the relevant theorem development is explicitly sorry-backed and its definition does not include Matsumura’s general defining-family object; it is not credited as a route. No other complete compatible external owner was found.
Corollary: principal ideals from symbolic powers
In a Krull ring, a nonzero principal ideal is the intersection over height-one primes of the symbolic powers prescribed by the corresponding normalised valuations.
Not formalized. Pinned/current Mathlib contains no Krull-ring/domain predicate matching Matsumura §12. GitHub-wide search found an experimental IsKrullDomain in acmepjz/lean-iwasawa, but the relevant theorem development is explicitly sorry-backed and its definition does not include Matsumura’s general defining-family object; it is not credited as a route. No other complete compatible external owner was found.
Theorem: Theorem 12.4
Every Noetherian normal domain is Krull. Suitable locally finite intersections of Krull rings in an overfield are Krull. If A is Krull, then A[X] and AX are Krull.
Not formalized. Pinned/current Mathlib contains no Krull-ring/domain predicate matching Matsumura §12. GitHub-wide search found an experimental IsKrullDomain in acmepjz/lean-iwasawa, but the relevant theorem development is explicitly sorry-backed and its definition does not include Matsumura’s general defining-family object; it is not credited as a route. No other complete compatible external owner was found.
Theorem: Theorem 12.5
Dedekind rings are exactly one-dimensional Krull rings.
Not formalized. Pinned/current Mathlib contains no Krull-ring/domain predicate matching Matsumura §12. GitHub-wide search found an experimental IsKrullDomain in acmepjz/lean-iwasawa, but the relevant theorem development is explicitly sorry-backed and its definition does not include Matsumura’s general defining-family object; it is not credited as a route. No other complete compatible external owner was found.
Theorem: Theorem 12.6
For a Krull ring, prescribed integer values at finitely many distinct height-one primes can be realized by an element of the fraction field while remaining nonnegative at every other height-one prime.
Not formalized. Pinned/current Mathlib contains no Krull-ring/domain predicate matching Matsumura §12. GitHub-wide search found an experimental IsKrullDomain in acmepjz/lean-iwasawa, but the relevant theorem development is explicitly sorry-backed and its definition does not include Matsumura’s general defining-family object; it is not credited as a route. No other complete compatible external owner was found.
Theorem: Theorem 12.7 (Mori-Nishimura)
If A is Krull and A/p is Noetherian for every height-one prime p, then A is Noetherian.
Not formalized. Pinned/current Mathlib contains no Krull-ring/domain predicate matching Matsumura §12. GitHub-wide search found an experimental IsKrullDomain in acmepjz/lean-iwasawa, but the relevant theorem development is explicitly sorry-backed and its definition does not include Matsumura’s general defining-family object; it is not credited as a route. No other complete compatible external owner was found.
Remark: normalisation can be non-Noetherian
The integral closure of a Noetherian domain in its fraction field is always Krull but can fail to be Noetherian.
Not formalized. Pinned/current Mathlib contains no Krull-ring/domain predicate matching Matsumura §12. GitHub-wide search found an experimental IsKrullDomain in acmepjz/lean-iwasawa, but the relevant theorem development is explicitly sorry-backed and its definition does not include Matsumura’s general defining-family object; it is not credited as a route. No other complete compatible external owner was found.