Theorem DedekindDomain.ProdAdicCompletions.isFiniteAdele_iff

Modification history

2025-04-23 09:49
Mathlib/RingTheory/DedekindDomain/FiniteAdeleRing.lean
chore(RingTheory/DedekindDomain/FiniteAdeleRing): refactor finite adeles (#23542) …
Deleted DedekindDomain.ProdAdicCompletions.isFiniteAdele_iffView on Github →
2024-06-26 12:43
Mathlib/RingTheory/DedekindDomain/FiniteAdeleRing.lean
feat: the finite adele ring is an algebra over the finite integral adeles. (#13705)
Added DedekindDomain.ProdAdicCompletions.isFiniteAdele_iffView on Github →