feat(RingTheory/Valuation/PrimeMultiplicity): define WithTop ℤ-valued prime multiplicity on a fraction field

[Command-Master]

Moves:

• multiplicity_addValuation -> AddValuation.multiplicity
• multiplicity_addValuation_apply -> AddValuation.multiplicity_apply

---

• depends on: Add toWithTop, ofWithTop #19164 [can also be adapted to depend on [Merged by Bors] - feat: add ENat.map and lemmas #19149 instead]
• depends on: [Merged by Bors] - feat(RingTheory/Valuation/Basic): API for conversion AddValuation ↔ Valuation #18786
• depends on: [Merged by Bors] - feat(Algebra/Order/Monoid/Unbundled/WithTop): add lemmas about WithTop.map and WithBot.map #19122
• depends on: feat(Algebra/Order/AddGroupWithTop): lemmas about LinearOrderedAddCommGroupWithTop #18954

[github-actions]

PR summary 12140a9a2d

Import changes exceeding 2%

%	File
+15.49%	Mathlib.RingTheory.Valuation.PrimeMultiplicity

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.RingTheory.Valuation.PrimeMultiplicity	975	1126	+151 (+15.49%)
Mathlib.RingTheory.DiscreteValuationRing.Basic	1140	1153	+13 (+1.14%)
Mathlib.Data.ENat.Basic	499	504	+5 (+1.00%)

Import changes for all files

Files	Import difference
18 files Mathlib.RingTheory.FractionalIdeal.Norm Mathlib.RingTheory.DedekindDomain.Dvr Mathlib.NumberTheory.NumberField.Discriminant.Basic Mathlib.NumberTheory.NumberField.FractionalIdeal Mathlib.NumberTheory.NumberField.EquivReindex Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone Mathlib.RingTheory.Ideal.Norm.AbsNorm Mathlib.RingTheory.Ideal.Norm.RelNorm Mathlib.RingTheory.DiscreteValuationRing.TFAE Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody Mathlib.RingTheory.DedekindDomain.Different Mathlib.NumberTheory.NumberField.Units.DirichletTheorem Mathlib.NumberTheory.NumberField.Units.Regulator Mathlib.RingTheory.Trace.Quotient Mathlib.NumberTheory.NumberField.House Mathlib.NumberTheory.NumberField.ClassNumber Mathlib.RingTheory.DedekindDomain.PID Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic	1
Mathlib.Analysis.Polynomial.CauchyBound	2
Mathlib.Data.Real.ENatENNReal	3
56 files Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative Mathlib.RingTheory.Polynomial.Ideal Mathlib.NumberTheory.Multiplicity Mathlib.Algebra.Polynomial.SpecificDegree Mathlib.RingTheory.UniqueFactorizationDomain.GCDMonoid Mathlib.NumberTheory.ArithmeticFunction Mathlib.RingTheory.UniqueFactorizationDomain.Basic Mathlib.RingTheory.UniqueFactorizationDomain.Nat Mathlib.Algebra.Polynomial.HasseDeriv Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet Mathlib.Data.Nat.Squarefree Mathlib.Data.Nat.Factorization.Induction Mathlib.RingTheory.UniqueFactorizationDomain.Finite Mathlib.Data.Nat.Factorization.Defs Mathlib.RingTheory.Localization.Away.Basic Mathlib.Algebra.Polynomial.RingDivision Mathlib.Algebra.Polynomial.Taylor Mathlib.RingTheory.Polynomial.IntegralNormalization Mathlib.RingTheory.MvPolynomial.Homogeneous Mathlib.Algebra.Squarefree.Basic Mathlib.Topology.Instances.ENat Mathlib.RingTheory.Radical Mathlib.RingTheory.Polynomial.HilbertPoly Mathlib.Algebra.Polynomial.Mirror Mathlib.Algebra.Polynomial.PartialFractions Mathlib.Algebra.Order.Antidiag.Nat Mathlib.Algebra.Polynomial.Monic Mathlib.NumberTheory.SmoothNumbers Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity Mathlib.RingTheory.MvPolynomial.EulerIdentity Mathlib.Algebra.Polynomial.Laurent Mathlib.RingTheory.MvPolynomial.Groebner Mathlib.RingTheory.ChainOfDivisors Mathlib.Algebra.MvPolynomial.SchwartzZippel Mathlib.Data.Nat.Choose.Factorization Mathlib.NumberTheory.MaricaSchoenheim Mathlib.Algebra.CharP.ExpChar Mathlib.RingTheory.UniqueFactorizationDomain.Finsupp Mathlib.Algebra.Polynomial.GroupRingAction Mathlib.Data.Nat.Factorization.Root Mathlib.Algebra.Polynomial.BigOperators Mathlib.RingTheory.Localization.NumDen Mathlib.Algebra.Polynomial.Reverse Mathlib.Algebra.Polynomial.SumIteratedDerivative Mathlib.Data.Nat.Factorization.Basic Mathlib.RingTheory.MvPowerSeries.Order Mathlib.RingTheory.MvPolynomial.MonomialOrder Mathlib.Algebra.Polynomial.CoeffMem Mathlib.Algebra.Polynomial.Lifts Mathlib.RingTheory.PowerSeries.Order Mathlib.Algebra.Polynomial.UnitTrinomial Mathlib.Algebra.Polynomial.Roots Mathlib.Data.Nat.Factorization.PrimePow Mathlib.Algebra.Polynomial.Degree.TrailingDegree Mathlib.Algebra.Polynomial.Div	4
27 files Mathlib.NumberTheory.Padics.PadicNorm Mathlib.NumberTheory.Padics.MahlerBasis Mathlib.RingTheory.Multiplicity Mathlib.Data.ENat.Basic Mathlib.RingTheory.WittVector.Compare Mathlib.Combinatorics.SimpleGraph.Diam Mathlib.Combinatorics.SimpleGraph.Girth Mathlib.Combinatorics.SimpleGraph.Metric Mathlib.Data.Nat.Multiplicity Mathlib.Data.ENat.BigOperators Mathlib.Combinatorics.SimpleGraph.Partition Mathlib.NumberTheory.Padics.PadicVal.Basic Mathlib.NumberTheory.Padics.RingHoms Mathlib.Order.Height Mathlib.RingTheory.WittVector.Isocrystal Mathlib.Combinatorics.SimpleGraph.ConcreteColorings Mathlib.Algebra.CharP.Reduced Mathlib.Data.Nat.PartENat Mathlib.Data.ENat.Lattice Mathlib.Topology.KrullDimension Mathlib.Algebra.CharP.Lemmas Mathlib.NumberTheory.Padics.PadicVal.Defs Mathlib.NumberTheory.Padics.ProperSpace Mathlib.RingTheory.WittVector.FrobeniusFractionField Mathlib.RingTheory.WittVector.DiscreteValuationRing Mathlib.Combinatorics.SimpleGraph.Coloring Mathlib.Order.KrullDimension	5
Mathlib.Topology.Algebra.Valued.LocallyCompact	8
6 files Mathlib.NumberTheory.LSeries.HurwitzZetaValues Mathlib.RingTheory.PowerSeries.Derivative Mathlib.NumberTheory.ZetaValues Mathlib.NumberTheory.BernoulliPolynomials Mathlib.NumberTheory.Bernoulli Mathlib.RingTheory.PowerSeries.Inverse	9
Mathlib.NumberTheory.Padics.Hensel	10
Mathlib.NumberTheory.Padics.PadicIntegers Mathlib.RingTheory.DiscreteValuationRing.Basic	13
Mathlib.RingTheory.Valuation.PrimeMultiplicity	151

---

Declarations diff

+ _root_.multiplicity_addValuation
+ _root_.multiplicity_addValuation_apply
+ adicValuation
+ adicValuation_coe
+ adicValuation_coe_pos_iff
+ adicValuation_neg_iff
+ adicValuation_pos_iff
+ injective_add_ne_top
+ le_map
+ lt_map
+ map_le
+ map_lt
+ multiplicity
+ multiplicity_apply
+ ofWithTop
+ ofWithTop_eq_ofNat_iff
+ ofWithTop_eq_some_iff
+ ofWithTop_eq_top_iff
+ ofWithTop_ofNat
+ ofWithTop_some
+ ofWithTop_symm
+ ofWithTop_toWithTop
+ ofWithTop_top
+ strictMono_add_ne_top
+ sub_pos
+ toWithTop
+ toWithTop_coe
+ toWithTop_eq_coe_iff
+ toWithTop_eq_ofNat_iff
+ toWithTop_eq_top_iff
+ toWithTop_ofNat
+ toWithTop_ofWithTop
+ toWithTop_symm
+ toWithTop_top
- multiplicity_addValuation
- multiplicity_addValuation_apply

You can run this locally as follows

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

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

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

---

No changes to technical debt.

You can run this locally as

./scripts/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).

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• Add toWithTop, ofWithTop #19164
• [Merged by Bors] - feat(RingTheory/Valuation/Basic): API for conversion AddValuation ↔ Valuation #18786
• [Merged by Bors] - feat(Algebra/Order/Monoid/Unbundled/WithTop): add lemmas about WithTop.map and WithBot.map #19122
• feat(Algebra/Order/AddGroupWithTop): lemmas about LinearOrderedAddCommGroupWithTop #18954
  By Dependent Issues (🤖). Happy coding!