Def NumberField.IdeleGroup.ofCompletion

Modification history

2026-08-27 17:33

Mathlib/NumberTheory/NumberField/AdeleRing.lean

feat(NumberTheory/NumberField/AdeleRing): define the idele class group (#40735) …

Added NumberField.IdeleGroup.ofCompletion View on Github →