Def NumberField.InfiniteAdeleRing

Modification history

2025-01-06 07:01
Mathlib/NumberTheory/NumberField/AdeleRing.lean
chore(NumberTheory/NumberField/AdeleRing): refactor adele rings (#20500) …
Modified NumberField.InfiniteAdeleRingView on Github →
2024-12-07 04:52
Mathlib/NumberTheory/NumberField/AdeleRing.lean
chore(Mathlib/NumberTheory/NumberField/*): rename completion -> Completion (#19646) …
Modified NumberField.InfiniteAdeleRingView on Github →
2024-11-09 14:40
Mathlib/NumberTheory/NumberField/AdeleRing.lean
feat: the adele ring of a number field (#16485) …
Added NumberField.InfiniteAdeleRingView on Github →