[Merged by Bors] - feat: the finite adele ring is an algebra over the finite integral adeles.

[kbuzzard]

---

We change the definition of the finite adeles to a subtype, and rework the original construction to be a subalgebra with this underlying subtype. We then show that the finite adeles are an algebra over the finite integral adeles, in an attempt to demonstrate that this set-up works fine.

[github-actions]

PR summary b23e33fe8c

Import changes

No significant changes to the import graph

---

Declarations diff

+ instance : Algebra (R_hat R K) (FiniteAdeleRing R K)
+ instance : Algebra K (FiniteAdeleRing R K)
+ instance : CommRing (FiniteAdeleRing R K)
+ isFiniteAdele_iff
+ subalgebra
- instance : Algebra K (FiniteAdeleRing R K) := Subalgebra.algebra _
- instance : CommRing (FiniteAdeleRing R K) := Subalgebra.toCommRing _

You can run this locally as follows

## summary with just the declaration names:
./scripts/no_lost_declarations.sh short <optional_commit>

## more verbose report:
./scripts/no_lost_declarations.sh <optional_commit>

[mariainesdff]

mantainer merge

[Ruben-VandeVelde]

maintainer merge

[github-actions]

🚀 Pull request has been placed on the maintainer queue by Ruben-VandeVelde.

[riccardobrasca]

LGTM to me, but let's keep an eye on it if it becomes too slow (we may need to do the same as we did for the ring of integers). Thanks!

bors merge

[ocfnash]

Thanks, two optional suggestions.

[ocfnash]

bors d+

[mathlib-bors]

✌️ kbuzzard can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[riccardobrasca]

bors r-

let's take Oliver's comments into account

[mathlib-bors]

Canceled.

[kbuzzard]

Finally taken into account!

bors r+

[mathlib-bors]

Canceled.

[kbuzzard]

bors r+

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style