Theorem NumberField.InfiniteAdeleRing.ringEquiv_mixedSpace_apply

Modification history

2026-07-29 08:07
Mathlib/NumberTheory/NumberField/InfiniteAdeleRing.lean
feat: notation for adele rings (#40535) …
Modified NumberField.InfiniteAdeleRing.ringEquiv_mixedSpace_applyView on Github →
2025-12-17 04:46
Mathlib/NumberTheory/NumberField/AdeleRing.lean
chore(NumberTheory/NumberField/AdeleRing): split file (#32897) …
Modified NumberField.InfiniteAdeleRing.ringEquiv_mixedSpace_applyView on Github →
2024-11-09 14:40
Mathlib/NumberTheory/NumberField/AdeleRing.lean
feat: the adele ring of a number field (#16485) …
Added NumberField.InfiniteAdeleRing.ringEquiv_mixedSpace_applyView on Github →