Commit 2025-04-23 09:49 1db99336

chore(RingTheory/DedekindDomain/FiniteAdeleRing): refactor finite adeles (#23542) Now we have a general theory of restricted products, we can refactor mathlib's finite adele file, removing the auxiliary results which are unused outside this file and replacing everything with much slicker proofs. Crucially, we also have a far more conceptual definition of the topology on the finite adele ring -- this is the big win. The motivation for this refactor is that the FLT project needs many more results about finite adeles (for example local compactness in the number field case) and this will be very easy to prove with this new definition (using RestrictedProduct.locallyCompactSpace_of_addGroup), whereas it took an entire project https://github.com/smmercuri/adele-ring_locally-compact with our current approach.