Def NumberField.AdeleRing.ofAdicCompletion

Modification history

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