Commit 2024-07-28 16:59 caac5b13

View on Github →

feat: topology on ring of finite adeles. (#14176) Use SubmodulesRingBasis to put a topology on the finite adeles.

Estimated changes

Modified Mathlib/RingTheory/DedekindDomain/AdicValuation.lean

added theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.mul_nonZeroDivisor_mem_adicCompletionIntegers

added theorem IsDedekindDomain.HeightOneSpectrum.coe_mem_adicCompletionIntegers

added theorem IsDedekindDomain.HeightOneSpectrum.intValuationDef_zero

added theorem IsDedekindDomain.HeightOneSpectrum.not_mem_adicCompletionIntegers

added theorem IsDedekindDomain.HeightOneSpectrum.valuation_eq_intValuationDef

added theorem IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_eq_valuation'

added theorem IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_eq_valuation

Modified Mathlib/RingTheory/DedekindDomain/FiniteAdeleRing.lean

added theorem DedekindDomain.FiniteAdeleRing.exists_finiteIntegralAdele_iff

added theorem DedekindDomain.FiniteAdeleRing.mul_nonZeroDivisor_mem_finiteIntegralAdeles

added theorem DedekindDomain.FiniteAdeleRing.submodulesRingBasis