Def NumberField.IdeleClassGroup.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.IdeleClassGroup.ofAdicCompletionView on Github →