subtype or coerced subring?

Stream: mathlib4

[Kevin Buzzard]

Recently (#12386) RingOfIntegers was promoted from a subalgebra to a type. I propose doing the same thing to docs#DedekindDomain.finiteAdeleRing , because K_hat, a.k.a. $\prod_{v<\infty} K_v$, the thing it's a subring of, is an auxiliary object whereas finiteAdeleRing a.k.a. $\mathbb{A}_K^f$ is used as a ring, e.g. you tensor things with it, put a topology on it, consider $GL_n$ of it and so on, so I think it deserves to be a type.

I made it a type in #13021 by just literally writing : Type _ after the definition, and then leaving it as a sub-K-algebra (the main contribution of the PR is beefing up the subring structure to a subalgebra structure). But the underlying type is a subtype of K_hat defined by a predicate isFiniteAdele, so I could literally define finiteAdeleRing (or rather FiniteAdeleRing) as a subtype and then put a ring structure on it afterwards. As it is, it's defined as a subring so inherits a ring structure when promoted to a type. Is there any preference between leaving it like this ("define as a subring/subalgebra and then coerce to a type") and redefining it as {x : K_hat / x.IsFiniteAdele} and then building the ring structure on the subtype directly?

[Yaël Dillies]

Both definitions have the same defeq, right?

[Yaël Dillies]

Personally I'd prefer the "coercion of subalgebra" approach

[Yaël Dillies]

For future reference: https://github.com/leanprover-community/mathlib4/wiki/Tradeoffs-of-concrete-types-defined-as-subobjects