Def IsDedekindDomain.FiniteAdeleRing.ofAdicCompletion

Modification history

2026-08-27 17:33
Mathlib/RingTheory/DedekindDomain/FiniteAdeleRing.lean
feat(NumberTheory/NumberField/AdeleRing): define the idele class group (#40735) …
Added IsDedekindDomain.FiniteAdeleRing.ofAdicCompletionView on Github →