Commit 2024-05-28 11:04 2ce120c4

View on Github →

feat: add API for finite adele rings (#13021) Let R be a Dedekind domain with field of fractions K. This PR does two things:

  1. makes the finite adeles of K/R into a K-algebra
  2. turns finiteAdeleRing into a type rather than a subring (because it's most definitely an important object of study in its own right, e.g. it needs a topology, and I don't want to end up in the same kind of hell that we had with rings of integers before they were a type). Note that this is a leaf file which I intend to develop a fair bit more in the near future.

Estimated changes