Commit 2025-11-27 16:30 d855d707

feat: PadicInt is isomorphic to the integers of the uniform space completion (Rat.padicValuation p).Completion (#30363)

• Uniform and ring isomorphisms between 𝒪[(Rat.padicValuation p).Completion] and ℤ_[p]
• A homeomorphism e : X ≃ Y gives a closed set { x : X | p x ↔ q (e x) } for clopen subsets given by p and q
• Move Padic.isUnit_den to an earlier file to avoid having to import Padics.RingHoms unnecessarily