feat: `v.adicCompletionIntegers K` is compact#21847

Closed

smmercuri wants to merge 33 commits intomasterfrom

AdicCompletionIntegersFiniteResidueField

Commits on Jan 27, 2025

Powers of uniformizers tend to zero in v-adic completion
Salvatore Mercuri
committed
The subspace and adelic topologies on the integral adeles coincide
Salvatore Mercuri
committed
The finite adele ring is locally compact if the ring of integers are compact
Salvatore Mercuri
committed

Commits on Jan 28, 2025

Refactor and documentation
Salvatore Mercuri
committed
Naming
Salvatore Mercuri
committed
powers of x tend to zero in adicValuation if x has valuation at most -1
Salvatore Mercuri
committed
Units val is coe of unitsWithZeroEquiv
Salvatore Mercuri
committed
Remove unnecessary import
Salvatore Mercuri
committed
Remove unnecessary import
Salvatore Mercuri
committed
use MonoidHomClass instead of new result
Salvatore Mercuri
committed
Merge main
Salvatore Mercuri
committed

Commits on Jan 29, 2025

Merge master
Salvatore Mercuri
committed
unitsWithzeroEquiv lemma name fix
Salvatore Mercuri
committed
Reverse rw direction
Salvatore Mercuri
committed

Commits on Jan 31, 2025

Abstract tendsto result to integer-valued rings
Salvatore Mercuri
committed

Commits on Feb 9, 2025

uniformity subcover
Salvatore Mercuri
committed
Merge dependent branch
Salvatore Mercuri
committed
Refine proofs
Salvatore Mercuri
committed

Commits on Feb 12, 2025

The ring of integers are compact whenever it is a DVR and the residue field is finite
Salvatore Mercuri
committed

Commits on Feb 13, 2025

Scratch proof for adicCompletionIntegers compact
Salvatore Mercuri
committed
Merge branch 'master' of https://github.com/leanprover-community/mathlib4 into AdicCompletionIntegersFiniteResidueField
Salvatore Mercuri
committed
Merge branch 'FiniteAdeleRingLocallyCompact' into AdicCompletionIntegersFiniteResidueField
Salvatore Mercuri
committed
Adele ring of a number field is locally compact
Salvatore Mercuri
committed

Commits on Feb 17, 2025

Merge branch 'master' of https://github.com/leanprover-community/mathlib4 into AdicCompletionIntegersFiniteResidueField
Salvatore Mercuri
committed
Merge branch 'master' of https://github.com/leanprover-community/mathlib4 into AdicCompletionIntegersFiniteResidueField
Salvatore Mercuri
committed
Comap results
Salvatore Mercuri
committed
Comap results
Salvatore Mercuri
committed

Commits on Feb 18, 2025

proof of algebraMap_mem_integers
Salvatore Mercuri
committed
proof of algebraMap_mem_integers
Salvatore Mercuri
committed
Move integer_isClosed
Salvatore Mercuri
committed

Commits on Mar 13, 2025

Merge master
Salvatore Mercuri
committed

Commits on Mar 14, 2025

Merge parent branch
Salvatore Mercuri
committed
Merge branch 'master' of https://github.com/leanprover-community/mathlib3 into AdicCompletionIntegersFiniteResidueField
Salvatore Mercuri
committed