Def NumberField.IdeleGroup.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.IdeleGroup.ofAdicCompletion View on Github →