English
AdeleRing(R,K) is defined as the product of the infinite adèle ring of K with the finite adèle ring of R over K; this generalizes the Adele ring to incorporate both integral and fractional data.
Русский
AdeleRing(R,K) задаётся как произведение бесконечного аделя над K и конечного аделя над R; обобщение адель кольца, включающее целочисленные и дробные данные.
LaTeX
$$$\\text{AdeleRing}(R,K) := \\text{InfiniteAdeleRing}(K) \\times \\text{FiniteAdeleRing}(R,K)$$$
Lean4
/-- `AdeleRing (𝓞 K) K` is the adele ring of a number field `K`.
More generally `AdeleRing R K` can be used if `K` is the field of fractions
of the Dedekind domain `R`. This enables use of rings like `AdeleRing ℤ ℚ`, which
in practice are easier to work with than `AdeleRing (𝓞 ℚ) ℚ`.
Note that this definition does not give the correct answer in the function field case.
-/
def AdeleRing (R K : Type*) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] :=
InfiniteAdeleRing K × FiniteAdeleRing R K
