Commit 2026-07-29 08:07 21da9fc4

View on Github →

feat: notation for adele rings (#40535) Notation:

K∞ : NumberField.InfiniteAdeleRing K;
𝔸ᶠ[R, K]: IsDedekindDomain.FiniteAdeleRing R K;
𝔸[R, K] : NumberField.AdeleRing R K;
specialisations 𝔸ᶠ[K] and 𝔸[K] to R = RingOfIntegers K.

Estimated changes

Modified Mathlib/NumberTheory/NumberField/AdeleRing.lean

modified theorem NumberField.AdeleRing.algebraMap_injective

Modified Mathlib/NumberTheory/NumberField/InfiniteAdeleRing.lean

modified theorem NumberField.InfiniteAdeleRing.algebraMap_apply

modified theorem NumberField.InfiniteAdeleRing.denseRange_algebraMap

modified theorem NumberField.InfiniteAdeleRing.norm_def

modified theorem NumberField.InfiniteAdeleRing.norm_eq_zero_of_not_isUnit

modified theorem NumberField.InfiniteAdeleRing.ringEquiv_mixedSpace_apply

Modified Mathlib/RingTheory/DedekindDomain/FiniteAdeleRing.lean

modified theorem IsDedekindDomain.FiniteAdeleRing.ext

modified theorem IsDedekindDomain.FiniteAdeleRing.infinite_valued_ne_one_of_not_isUnit

modified theorem IsDedekindDomain.FiniteAdeleRing.isUnit_iff

modified def IsDedekindDomain.FiniteAdeleRing.unitEmbedding

modified theorem IsDedekindDomain.FiniteAdeleRing.unitEmbedding_apply

modified theorem IsDedekindDomain.FiniteAdeleRing.unitsEquiv_finite_valued_eq_one