Commit 2024-06-26 12:43 9741ec32

View on Github →

feat: the finite adele ring is an algebra over the finite integral adeles. (#13705)

Estimated changes

Modified Mathlib/RingTheory/DedekindDomain/FiniteAdeleRing.lean

added def DedekindDomain.FiniteAdeleRing.subalgebra

modified def DedekindDomain.FiniteAdeleRing

added theorem DedekindDomain.ProdAdicCompletions.isFiniteAdele_iff