Commit 2025-01-06 07:01 10a42154

View on Github →

chore(NumberTheory/NumberField/AdeleRing): refactor adele rings (#20500) The current AdeleRing ℚ explicitly involves 𝓞 ℚ and is not much fun to work with. This PR enables AdeleRing ℤ ℚ.

Estimated changes

Modified Mathlib/NumberTheory/NumberField/AdeleRing.lean

modified theorem NumberField.AdeleRing.algebraMap_injective

modified theorem NumberField.AdeleRing.algebraMap_snd_apply

modified def NumberField.AdeleRing

modified def NumberField.InfiniteAdeleRing