Commit 2026-06-08 09:51 e973e031

feat(DedekindDomain/AdicValuation): intValuation on uniformizers is exp (-1) (#37501) This PR adds the lemma intValuation_uniformizer which is an application of #37497. Note that I've had to reorganize the files a little bit:

1. I wanted to import Valuation.Discrete.Basic in AdicValuation but this was not possible since there was a dependency in the other direction (Valuation.Discrete.Basic depended on AdicValuation). I don't think this makes sense - we want to have access to basic definitions on general valuation in an application file like AdicValuation. The reorganization consist of moving the IsDiscreteValuationRing of Valuation.Discrete.Basic to AdicValuation. The reorganization consist of moving the IsDiscreteValuationRing section to a new file.
2. I moved some lemmas out of Mathlib.RingTheory.Valuation.Discrete.RankOne to the parent file Mathlib.RingTheory.Valuation.Discrete.Basic.. These lemmas do not need the richer imports from RankOne and are needed in my application. AI disclaimer : I used Claude to give me some feedback on the PR.