[Merged by Bors] - feat(RingTheory): Order of vanishing in a discrete valuation ring

[Raph-DG]

In this PR we develop some API for working with the order of vanishing in a discrete valuation ring.

---

[github-actions]

PR summary 062adc5c07

Import changes exceeding 2%

%	File
+7.43%	Mathlib.RingTheory.DiscreteValuationRing.TFAE

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.RingTheory.DiscreteValuationRing.TFAE	1723	1851	+128 (+7.43%)
Mathlib.RingTheory.DedekindDomain.AdicValuation	2235	2243	+8 (+0.36%)
Mathlib.RingTheory.Valuation.Discrete.Basic	2239	2247	+8 (+0.36%)

Import changes for all files

Files	Import difference
Mathlib.RingTheory.OrderOfVanishing	-1843
12 files Mathlib.NumberTheory.FLT.Three Mathlib.NumberTheory.NumberField.Cyclotomic.Basic Mathlib.NumberTheory.NumberField.Cyclotomic.Galois Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal Mathlib.NumberTheory.NumberField.Cyclotomic.PID Mathlib.NumberTheory.NumberField.Cyclotomic.Three Mathlib.NumberTheory.NumberField.Discriminant.Different Mathlib.NumberTheory.NumberField.Ideal.Basic Mathlib.NumberTheory.RamificationInertia.Unramified Mathlib.RingTheory.DedekindDomain.Different Mathlib.RingTheory.DedekindDomain.LinearDisjoint Mathlib.RingTheory.Unramified.Dedekind	3
26 files Mathlib.Analysis.Fourier.ZMod Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar Mathlib.NumberTheory.DirichletCharacter.GaussSum Mathlib.NumberTheory.Fermat Mathlib.NumberTheory.GaussSum Mathlib.NumberTheory.Height.NumberField Mathlib.NumberTheory.JacobiSum.Basic Mathlib.NumberTheory.LSeries.DirichletContinuation Mathlib.NumberTheory.LSeries.Nonvanishing Mathlib.NumberTheory.LSeries.PrimesInAP Mathlib.NumberTheory.LSeries.ZMod Mathlib.NumberTheory.LSeries.ZetaZeros Mathlib.NumberTheory.LegendreSymbol.AddCharacter Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity Mathlib.NumberTheory.LucasLehmer Mathlib.NumberTheory.MahlerMeasure Mathlib.NumberTheory.NumberField.AdeleRing Mathlib.NumberTheory.NumberField.CMField Mathlib.NumberTheory.NumberField.Completion.FinitePlace Mathlib.NumberTheory.NumberField.Cyclotomic.Embeddings Mathlib.NumberTheory.NumberField.FinitePlaces Mathlib.NumberTheory.NumberField.ProductFormula Mathlib.Tactic.NormNum.LegendreSymbol Mathlib.Tactic	6
32 files Mathlib.AlgebraicGeometry.EllipticCurve.Reduction Mathlib.FieldTheory.Laurent Mathlib.FieldTheory.RatFunc.AsPolynomial Mathlib.FieldTheory.RatFunc.Degree Mathlib.FieldTheory.RatFunc.IntermediateField Mathlib.FieldTheory.RatFunc.Luroth Mathlib.NumberTheory.ClassNumber.FunctionField Mathlib.NumberTheory.Cyclotomic.Basic Mathlib.NumberTheory.Cyclotomic.Discriminant Mathlib.NumberTheory.Cyclotomic.Gal Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots Mathlib.NumberTheory.FunctionField Mathlib.NumberTheory.Padics.HeightOneSpectrum Mathlib.NumberTheory.PrimesCongruentOne Mathlib.NumberTheory.RatFunc.Ostrowski Mathlib.RingTheory.DedekindDomain.AdicValuation Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing Mathlib.RingTheory.DedekindDomain.GaussLemma Mathlib.RingTheory.DedekindDomain.SInteger Mathlib.RingTheory.DedekindDomain.SelmerGroup Mathlib.RingTheory.LaurentSeries Mathlib.RingTheory.LittleWedderburn Mathlib.RingTheory.LocalRing.ResidueField.Polynomial Mathlib.RingTheory.Polynomial.Cyclotomic.Basic Mathlib.RingTheory.Polynomial.Cyclotomic.Eval Mathlib.RingTheory.Polynomial.Cyclotomic.Expand Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization Mathlib.RingTheory.Polynomial.Cyclotomic.Roots Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral Mathlib.RingTheory.RootsOfUnity.AlgebraicallyClosed Mathlib.RingTheory.Valuation.Discrete.Basic Mathlib.RingTheory.Valuation.Discrete.RankOne	8
Mathlib.NumberTheory.NumberField.DedekindZeta	23
13 files Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord Mathlib.NumberTheory.NumberField.ClassNumber Mathlib.NumberTheory.NumberField.Discriminant.Basic Mathlib.NumberTheory.NumberField.EquivReindex Mathlib.NumberTheory.NumberField.House Mathlib.NumberTheory.NumberField.Ideal.Asymptotics Mathlib.NumberTheory.NumberField.InfiniteAdeleRing Mathlib.NumberTheory.NumberField.Units.DirichletTheorem Mathlib.NumberTheory.NumberField.Units.Regulator	24
7 files Mathlib.Algebra.Lie.Basis Mathlib.Algebra.Lie.Weights.IsSimple Mathlib.Algebra.Lie.Weights.RootSystem Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basis Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple	29
3 files Mathlib.NumberTheory.RamificationInertia.Galois Mathlib.NumberTheory.RamificationInertia.HilbertTheory Mathlib.RingTheory.Ideal.Norm.RelNorm	30
19 files Mathlib.LinearAlgebra.RootSystem.BaseChange Mathlib.LinearAlgebra.RootSystem.BaseExists Mathlib.LinearAlgebra.RootSystem.Base Mathlib.LinearAlgebra.RootSystem.Basic Mathlib.LinearAlgebra.RootSystem.CartanMatrix Mathlib.LinearAlgebra.RootSystem.Chain Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear Mathlib.LinearAlgebra.RootSystem.Finite.G2 Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Lemmas Mathlib.LinearAlgebra.RootSystem.Hom Mathlib.LinearAlgebra.RootSystem.Irreducible Mathlib.LinearAlgebra.RootSystem.IsValuedIn Mathlib.LinearAlgebra.RootSystem.Reduced Mathlib.LinearAlgebra.RootSystem.RootPairingCat Mathlib.LinearAlgebra.RootSystem.RootPositive Mathlib.LinearAlgebra.RootSystem.WeylGroup Mathlib.RingTheory.Flat.TorsionFree	37
Mathlib.RingTheory.Trace.Quotient	98
Mathlib.RingTheory.DedekindDomain.Factorization	106
3 files Mathlib.NumberTheory.NumberField.FractionalIdeal Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind Mathlib.RingTheory.FractionalIdeal.Norm	109
6 files Mathlib.NumberTheory.RamificationInertia.Basic Mathlib.NumberTheory.RamificationInertia.Inertia Mathlib.RingTheory.Ideal.Int Mathlib.RingTheory.Ideal.Norm.AbsNorm Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients Mathlib.RingTheory.Localization.AtPrime.Extension	114
Mathlib.RingTheory.DedekindDomain.Instances	116
3 files Mathlib.NumberTheory.RamificationInertia.Ramification Mathlib.RingTheory.DedekindDomain.Dvr Mathlib.RingTheory.DedekindDomain.PID	117
Mathlib.RingTheory.DiscreteValuationRing.TFAE	128
Mathlib.RingTheory.OrderOfVanishing.Basic	1843
Mathlib.RingTheory.OrderOfVanishing.Noetherian (new file)	2267

---

Declarations diff

+ IsDiscreteValuationRing.not_krullDimLE_zero
+ IsDiscreteValuationRing.ringKrullDim_eq_one
+ MonoidWithZeroHom.comap_mker
+ addVal_eq_iff_associated
+ associated_of_ordFrac_eq
+ associated_of_valuation_eq
+ div_smul_div_comm
+ exists_units_eq_smul_zpow_of_irreducible
+ exp_eq_coe_ofAdd
+ instance [IsDomain R] [IsDiscreteValuationRing R] : KrullDimLE 1 R
+ intValuation_maximalIdeal
+ isSimpleModule_iff_isSimpleModule_of_algebraMap_surjective
+ isUnit_iff_ordFrac_one_of_isDiscreteValuationRing
+ min_inv_inv_le
+ mker_inverse
+ mker_ordFrac_eq_isUnitSubmonoid
+ mker_valuation_eq_isUnitSubmonoid
+ ordFrac_add
+ ordFrac_eq_intValuation
+ ordFrac_eq_inverse_comp_valuation
+ ordFrac_eq_valuation_inv
+ ordFrac_ge_one_of_ne_zero
+ ordFrac_irreducible
+ ordFrac_le_smul
+ ordFrac_of_isUnit
+ ordMonoidHom
+ ordMonoidHom_eq_ord
+ ordMonoidWithZeroHom_eq_coe
+ ordMonoidWithZeroHom_eq_intValuation
+ ordMonoidWithZeroHom_eq_ord
+ ordMonoidWithZeroHom_eq_ordMonoidHom
+ ordMonoidWithZeroHom_eq_zero
+ ordMonoidWithZeroHom_eq_zero_iff
+ ordMonoidWithZeroHom_isUnit
+ ordMonoidWithZeroHom_ne_zero
+ ord_add
+ ord_eq_addVal
+ ord_eq_iff_associated
+ ord_eq_of_associated
+ ord_le_iff
+ ord_le_ord_mul
+ ord_le_ord_of_dvd
+ ord_le_smul
+ ord_lt_top
+ ord_mul'
+ ord_mul_of_isUnit_left
+ ord_mul_of_isUnit_right
+ ord_ne_top
+ ord_neg
+ ord_of_irreducible
+ ord_of_isUnit
+ ord_pow
+ ord_smul_of_isUnit
+ ord_zero
+ orderIsoOfAlgebraMapSurjective
+ valuation_eq_one_iff_notMem

You can run this locally as follows

## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/reporting/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

---

note: file Mathlib/RingTheory/OrderOfVanishing.lean` was renamed to `Mathlib/RingTheory/OrderOfVanishing/Basic.lean without a module deprecation
Please create a follow-up pull request adding one. Thanks!

[mathlib4-merge-conflict-bot]

This pull request has conflicts, please merge master and resolve them.

[Copilot]

Pull request overview

This PR extends the Ring.ord / Ring.ordFrac API to better support “order of vanishing” computations in Noetherian rings (especially Krull dim ≤ 1) and in discrete valuation rings, connecting these notions to existing valuation/intValuation infrastructure.

Changes:

• Add a new OrderOfVanishing.Noetherian module with lemmas relating ord, ordFrac, DVR addVal, and (adic/discrete) valuations.
• Extend DVR/valuation files with lemmas identifying multiplicative kernels and relating equality of valuations to unit-scaling/association.
• Add a few general-purpose supporting lemmas (min_inv_inv_le, div_smul_div_comm, orderIsoOfAlgebraMapSurjective, etc.) and update Mathlib.lean imports.

Reviewed changes

Copilot reviewed 14 out of 14 changed files in this pull request and generated 2 comments.

Show a summary per file

File	Description
Mathlib/RingTheory/Valuation/Discrete/Basic.lean	Adds kernel/association lemmas for the DVR valuation and an intValuation computation lemma.
Mathlib/RingTheory/SimpleModule/Basic.lean	Adds a simplicity equivalence lemma assuming algebraMap is surjective.
Mathlib/RingTheory/OrderOfVanishing/Noetherian.lean	New file: Noetherian/DVR-focused API for ord/ordFrac and comparisons to valuations.
Mathlib/RingTheory/OrderOfVanishing/Basic.lean	Extends the base API (ord_pow, unit/scalar invariance, ordMonoidWithZeroHom tweaks).
Mathlib/RingTheory/DiscreteValuationRing/TFAE.lean	Adds Krull dimension lemmas/instances for DVRs.
Mathlib/RingTheory/DiscreteValuationRing/Basic.lean	Adds a decomposition lemma in the fraction field and addVal-associated equivalence.
Mathlib/RingTheory/DedekindDomain/AdicValuation.lean	Adds a simp lemma characterizing when the valuation equals 1.
Mathlib/Algebra/Order/Group/MinMax.lean	Adds min_inv_inv_le.
Mathlib/Algebra/GroupWithZero/WithZero.lean	Adds exp_eq_coe_ofAdd.
Mathlib/Algebra/GroupWithZero/Submonoid/Instances.lean	Adds MonoidWithZeroHom.mker_inverse.
Mathlib/Algebra/GroupWithZero/Action/Basic.lean	Adds div_smul_div_comm.
Mathlib/Algebra/Group/Subgroup/Actions.lean	Adds MonoidWithZeroHom.comap_mker.
Mathlib/Algebra/Algebra/Tower.lean	Adds Submodule.orderIsoOfAlgebraMapSurjective.
Mathlib.lean	Imports the new OrderOfVanishing modules.

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

[riccardobrasca]

There is just one comment left, but otherwise LGTM, thanks!

bors d+

[mathlib-bors]

✌️ Raph-DG can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[Raph-DG]

There is just one comment left, but otherwise LGTM, thanks!

bors d+

Awesome, just fixing that comment up now :) Thanks for all your help!

[Raph-DG]

bors r+

[riccardobrasca]

Don't forget to add the deprecated module in another PR!

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• ci (staging) / Post-Build Step
• ci (staging) / Lint style
• ci (staging) / Build
• ci (staging) / Post-CI job