Theorem Rat.HeightOneSpectrum.adicCompletionIntegers.coe_padicIntEquiv_symm_apply

Modification history

2025-12-19 16:47
Mathlib/NumberTheory/Padics/HeightOneSpectrum.lean
feat: `adicCompletion` for `Rat` is uniform isomorphic to `Padic` (#30576)
Added Rat.HeightOneSpectrum.adicCompletionIntegers.coe_padicIntEquiv_symm_applyView on Github →