Def NumberField.InfiniteAdeleRing.ofCompletion

Modification history

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