Commit 2023-06-22 21:12 39b465c3

View on Github →

feat: port RingTheory.DedekindDomain.FiniteAdeleRing (#5402)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/DedekindDomain/FiniteAdeleRing.lean

added def DedekindDomain.FiniteIntegralAdeles.Coe.addMonoidHom

added def DedekindDomain.FiniteIntegralAdeles.Coe.algHom

added theorem DedekindDomain.FiniteIntegralAdeles.Coe.algHom_apply

added def DedekindDomain.FiniteIntegralAdeles.Coe.ringHom

added theorem DedekindDomain.FiniteIntegralAdeles.coe_apply

added def DedekindDomain.FiniteIntegralAdeles

added theorem DedekindDomain.ProdAdicCompletions.IsFiniteAdele.add

added theorem DedekindDomain.ProdAdicCompletions.IsFiniteAdele.mul

added theorem DedekindDomain.ProdAdicCompletions.IsFiniteAdele.neg

added theorem DedekindDomain.ProdAdicCompletions.IsFiniteAdele.one

added theorem DedekindDomain.ProdAdicCompletions.IsFiniteAdele.zero

added def DedekindDomain.ProdAdicCompletions.IsFiniteAdele

added def DedekindDomain.ProdAdicCompletions

added theorem DedekindDomain.mem_finiteAdeleRing_iff