Commit 2025-12-01 21:12 6eabe6b2

chore: make FiniteAdeleRing a def rather than an abbrev (#32277) On current master #synth CommRing (FiniteAdeleRing A K) works fine but #synth SMul (FiniteAdeleRing A K) (FiniteAdeleRing A K) times out because typeclass inference can see through the abbrev and the first thing it tries is "if G acts on X_i for all i then G acts on the restricted product" and it goes off on a wild goose chase, quickly hitting dreaded stuff such as [] ✅️ apply @NormedAlgebra.toAlgebra to Algebra (FiniteAdeleRing A K) K ▶ , spending a long time failing on Group (FiniteAdeleRing A K) and so on. I claim that there is no need for typeclass inference to know that finite adele rings are actually restricted products; this is in some sense an implentation detail (the finite adele ring of a number field $K$ is just $K\otimes_{\mathbb{Z}}\widehat{\mathbb{Z}}$; the fact that we represent it as a restricted product is some sense a historical coincidence). Indeed, we have developed the theory of adeles and finite adeles a lot further in the FLT repo and there is only one place where we had an auxiliary restricted product of vector spaces and used typeclass inference to give a module structure over a finite adele ring; this was some internal object in a proof.