mathlib3

a8e7ac80 - feat(ring_theory/dedekind_domain/finite_adele_ring): add finite_adele_ring (#14249)

feat(ring_theory/dedekind_domain/finite_adele_ring): add finite_adele_ring (#14249) We define the finite adèle ring of a Dedekind domain and show that it is a commutative ring. Co-authored-by: Oliver Nash <github@olivernash.org>