Commit 2025-12-19 16:47 d4e7b767

View on Github →

feat: adicCompletion for Rat is uniform isomorphic to Padic (#30576)

Estimated changes

Modified Mathlib.lean

Created Mathlib/NumberTheory/Padics/HeightOneSpectrum.lean

added theorem PadicInt.coe_adicCompletionIntegersEquiv_apply

added theorem PadicInt.coe_adicCompletionIntegersEquiv_symm_apply

added theorem Rat.HeightOneSpectrum.adicCompletion.padicEquiv_bijOn

added theorem Rat.HeightOneSpectrum.adicCompletionIntegers.coe_padicIntEquiv_apply

added theorem Rat.HeightOneSpectrum.adicCompletionIntegers.coe_padicIntEquiv_symm_apply

added theorem Rat.HeightOneSpectrum.natGenerator_dvd_iff

added theorem Rat.HeightOneSpectrum.prime_natGenerator

added theorem Rat.HeightOneSpectrum.span_natGenerator

added theorem Rat.HeightOneSpectrum.valuation_equiv_padicValuation

added theorem Rat.int_algebraMap_injective

added theorem Rat.int_algebraMap_surjective

Modified Mathlib/RingTheory/DedekindDomain/Ideal/Lemmas.lean

added theorem map_prime_of_equiv

Modified Mathlib/Topology/Algebra/Algebra/Equiv.lean

added def ContinuousAlgEquiv.cast

added theorem ContinuousAlgEquiv.cast_apply

added theorem ContinuousAlgEquiv.cast_symm_apply

added theorem ContinuousAlgEquiv.surjective

Modified Mathlib/Topology/Algebra/Valued/WithVal.lean

added theorem Valuation.IsEquiv.valuedCompletion_le_one_iff

added theorem Valuation.exists_div_eq_of_surjective