Commit 2026-08-27 17:33 39c86ed8

View on Github →

feat(NumberTheory/NumberField/AdeleRing): define the idele class group (#40735) This PR defines the idele class group and the maps from the completions at finite places. This will be used to define Hecke L-Functions.

Estimated changes

Modified Mathlib/NumberTheory/NumberField/AdeleRing.lean

added def NumberField.AdeleRing.ofAdicCompletion

added def NumberField.AdeleRing.ofCompletion

modified def NumberField.AdeleRing

added def NumberField.IdeleClassGroup.ofAdicCompletion

added def NumberField.IdeleClassGroup.ofCompletion

added def NumberField.IdeleGroup.ofAdicCompletion

added def NumberField.IdeleGroup.ofCompletion

added def NumberField.IdeleGroup.unitEmbedding

Modified Mathlib/NumberTheory/NumberField/InfiniteAdeleRing.lean

added def NumberField.InfiniteAdeleRing.ofCompletion

Modified Mathlib/RingTheory/DedekindDomain/FiniteAdeleRing.lean

added def IsDedekindDomain.FiniteAdeleRing.ofAdicCompletion

Modified Mathlib/Topology/Algebra/RestrictedProduct/Basic.lean

added def RestrictedProduct.mulSingleMonoidHom