Commit 2025-12-17 04:46 6c8fd6fb

View on Github →

chore(NumberTheory/NumberField/AdeleRing): split file (#32897) The file NumberTheory/NumberField/AdeleRing.lean is not long but it's doing two different jobs: developing the theory of the infinite adele ring and of the adele ring. Why not do this in two files? This PR does nothing but the split (adding NumberTheory/NumberField/InfiniteAdeleRing.lean).

Estimated changes

Modified Mathlib.lean

Modified Mathlib/NumberTheory/NumberField/AdeleRing.lean

deleted theorem NumberField.InfiniteAdeleRing.algebraMap_apply

deleted theorem NumberField.InfiniteAdeleRing.denseRange_algebraMap

deleted theorem NumberField.InfiniteAdeleRing.mixedEmbedding_eq_algebraMap_comp

deleted theorem NumberField.InfiniteAdeleRing.ringEquiv_mixedSpace_apply

deleted def NumberField.InfiniteAdeleRing

Created Mathlib/NumberTheory/NumberField/InfiniteAdeleRing.lean

added theorem NumberField.InfiniteAdeleRing.algebraMap_apply

added theorem NumberField.InfiniteAdeleRing.denseRange_algebraMap

added theorem NumberField.InfiniteAdeleRing.mixedEmbedding_eq_algebraMap_comp

added theorem NumberField.InfiniteAdeleRing.ringEquiv_mixedSpace_apply

added def NumberField.InfiniteAdeleRing