Theorem DedekindDomain.ProdAdicCompletions.IsFiniteAdele.algebraMap'

Modification history

2025-04-23 09:49
Mathlib/RingTheory/DedekindDomain/FiniteAdeleRing.lean
chore(RingTheory/DedekindDomain/FiniteAdeleRing): refactor finite adeles (#23542) …
Deleted DedekindDomain.ProdAdicCompletions.IsFiniteAdele.algebraMap'View on Github →
2025-02-21 11:42
Mathlib/RingTheory/DedekindDomain/FiniteAdeleRing.lean
chore: make arg in HeightOneSpectrum.valuation explicit (#22139) …
Modified DedekindDomain.ProdAdicCompletions.IsFiniteAdele.algebraMap'View on Github →
2024-05-28 11:04
Mathlib/RingTheory/DedekindDomain/FiniteAdeleRing.lean
feat: add API for finite adele rings (#13021) …
Added DedekindDomain.ProdAdicCompletions.IsFiniteAdele.algebraMap'View on Github →