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