Theorem Rat.int_algebraMap_surjective

Modification history

2025-12-23 19:14
Mathlib/NumberTheory/Padics/HeightOneSpectrum.lean
fix: definition of `Rat.IsIntegralClosure.intEquiv` (#33203) …
Modified Rat.int_algebraMap_surjectiveView on Github →
2025-12-19 16:47
Mathlib/NumberTheory/Padics/HeightOneSpectrum.lean
feat: `adicCompletion` for `Rat` is uniform isomorphic to `Padic` (#30576)
Added Rat.int_algebraMap_surjectiveView on Github →