Theorem NumberField.AdeleRing.algebraMap_injective

Modification history

2025-01-06 07:01
Mathlib/NumberTheory/NumberField/AdeleRing.lean
chore(NumberTheory/NumberField/AdeleRing): refactor adele rings (#20500) …
Modified NumberField.AdeleRing.algebraMap_injectiveView on Github →
2024-11-09 14:40
Mathlib/NumberTheory/NumberField/AdeleRing.lean
feat: the adele ring of a number field (#16485) …
Added NumberField.AdeleRing.algebraMap_injectiveView on Github →