Commit 2026-10-09 07:54 95142c9c

View on Github →

feat: ValuativeRel and IsValuativeTopology (v.adicCompletion K) (#44279)

Prove IsValuativeTopology (v.adicCompletion K)
Make Valued instance on v.adicCompletion K be derived from IsValuativeTopology
Remove some usage of Valued.v from AdicValuation.lean

Estimated changes

Modified Mathlib/NumberTheory/Padics/HeightOneSpectrum.lean

Modified Mathlib/RingTheory/DedekindDomain/AdicValuation.lean

deleted theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.coe_valueGroupEquiv

added theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.coe_valueGroupMulEquiv

deleted theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.coe_valueGroupOrderIso_coe

deleted theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.embedding_valueGroupOrderIso

added theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.embedding_valueGroupOrderMonoidIso

added theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.extension_apply_eq_valued

added theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.valuationExtension_toCompletion

added theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.valuation_ofCompletion

deleted def IsDedekindDomain.HeightOneSpectrum.adicCompletion.valueGroupEquiv

added def IsDedekindDomain.HeightOneSpectrum.adicCompletion.valueGroupMulEquiv

deleted theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.valueGroupOrderIso_restrict

added theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.valueGroupOrderMonoidIso_coe

added theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.valueGroupOrderMonoidIso_restrict

added theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.valuedAdicCompletion_apply

deleted theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.valuedAdicCompletion_def

deleted theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.valued_ofCompletion

added theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.valued_ofCompletion_apply

deleted theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.valued_toCompletion

added theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.valued_toCompletion_apply

Modified Mathlib/RingTheory/LaurentSeries.lean

Modified Mathlib/RingTheory/Valuation/ValuativeRel/Basic.lean

added theorem Valuation.lt_div_iff_mul_vlt

Modified Mathlib/Topology/Algebra/ValuativeRel/ValuativeTopology.lean

added theorem IsValuativeTopology.of_isInducing