Commit 2026-07-09 14:13 8bba4200

View on Github →

refactor(NumberTheory): make adicCompletion a one-field structure (#41526) adicCompletion as an abbrev is causing slowdown in FLT.

Estimated changes

Modified Mathlib/NumberTheory/NumberField/Completion/FinitePlace.lean

Modified Mathlib/NumberTheory/Padics/HeightOneSpectrum.lean

Modified Mathlib/RingTheory/DedekindDomain/AdicValuation.lean

added theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.coe_add

added theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.coe_mul

added theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.coe_one

added theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.coe_toCompletion

added theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.coe_valueGroupEquiv

added theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.coe_valueGroupOrderIso_coe

added theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.coe_zero

added theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.continuous_ofCompletion

added theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.continuous_toCompletion

added theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.embedding_valueGroupOrderIso

added def IsDedekindDomain.HeightOneSpectrum.adicCompletion.equiv

added def IsDedekindDomain.HeightOneSpectrum.adicCompletion.equivCompletion

added theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext

added theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.isUniformInducing_toCompletion

added theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.ofCompletion_surjective

added theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.ofCompletion_toCompletion

added theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.toCompletion_add

added theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.toCompletion_mul

added theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.toCompletion_ofCompletion

added theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.toCompletion_one

added theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.toCompletion_surjective

added theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.toCompletion_zero

added def IsDedekindDomain.HeightOneSpectrum.adicCompletion.uniformEquiv

added def IsDedekindDomain.HeightOneSpectrum.adicCompletion.valueGroupEquiv

added theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.valueGroupOrderIso_restrict

added theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.valueGroup_eq

added theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.valuedAdicCompletion_def

added theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.valued_coe

added theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.valued_ofCompletion

added theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.valued_toCompletion

added structure IsDedekindDomain.HeightOneSpectrum.adicCompletion

added theorem IsDedekindDomain.HeightOneSpectrum.algebraMap_adicCompletion_toCompletion

modified theorem IsDedekindDomain.HeightOneSpectrum.denseRange_algebraMap

deleted theorem IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_def

Modified Mathlib/RingTheory/DedekindDomain/FiniteAdeleRing.lean

Modified Mathlib/RingTheory/LaurentSeries.lean