feat: algebraMap K L is uniform continuous with respect to adic topologies, when the ideal w of L lies above v

[smmercuri]

• A is a Dedekind domain with field of fractions K.
• B is a Dedekind domain with field of fractions L.
• L is a field extension of K.
• v is a height one prime ideal of A.
• w is a height one prime ideal of B lying over v.

Then respective valuations are related via the ramification index, and algebraMap (WithVal (v.valuation K)) (WithVal (w.valuation L)) is uniform continuous.

---

• depends on: fix: defeq abuse in WithVal #34049

[github-actions]

PR summary 28cc1a5eaa

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.NumberTheory.RamificationInertia.Valuation (new file)	2153

---

Declarations diff

+ Ideal.isPrime_of_irreducible
+ algebraMap_apply
+ algebraMap_apply'
+ emultiplicity_eq_zero_of_ne
+ emultiplicity_map_eq_ramificationIdx_mul
+ emultiplicity_map_eq_ramificationIdx_mul_of_prime
+ emultiplicity_map_eq_zero_of_ne
+ instance (priority := 99) : Coe R v.Completion
+ instance : CoeHead (𝓞 (WithVal v)) (WithVal v)
+ instance [CommRing S] [CommRing R] [Algebra S R] [IsFractionRing S R] (v : Valuation R Γ₀) :
+ instance [CommSemiring S] [Algebra S R] (v : Valuation R Γ₀) : Algebra S (WithVal v)
+ instance [Ring R] {Γ₀ : Type*} [LinearOrderedCommGroupWithZero Γ₀]
+ instance [Ring S] [Algebra R S] :
+ instance [Ring S] [Semiring P] [Module P R] [Module P S]
+ intValuation_eq_coe_neg_multiplicity
+ intValuation_liesOver
+ uniformContinuous_algebraMap_liesOver
+ valuation_liesOver
- instance : Coe R v.Completion
- instance : CoeHead (𝓞 (WithVal v)) (WithVal v) := inferInstanceAs (CoeHead (𝓞 K) K)
- instance [CommSemiring S] [CommRing R] [Algebra S R] (v : Valuation R Γ₀) :
- instance {P S : Type*} [Ring S] [Semiring P] [Module P R] [Module P S]
- instance {S : Type*} [Ring S] [Algebra R S] (w : Valuation S Γ₀) :
- instance {S : Type*} [Ring S] [Algebra R S] :

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:

• fix: defeq abuse in WithVal #34049
  By Dependent Issues (🤖). Happy coding!