Theorem NumberField.InfiniteAdeleRing.ringEquiv_mixedSpace_apply

Modification history

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 →