English
The finite adele ring is endowed with a natural algebra structure over R, built from the algebra map and the tower identifications.
Русский
Конечный адель наделяется естественной структурой algebra над R, порождаемой алгебраической картой и идентификациями башни.
LaTeX
$$definstAlgebra : Algebra R (IsDedekindDomain.FiniteAdeleRing R K)$$
Lean4
/-- If `K` is the field of fractions of the Dedekind domain `R` then `FiniteAdeleRing R K` is
the ring of finite adeles of `K`, defined as the restricted product of the completions
`K_v` with respect to the subrings `R_v`. Here `v` runs through the nonzero primes of `R`
and the restricted product is the subring of `∏_v K_v` consisting of elements which
are in `R_v` for all but finitely many `v`.
-/
abbrev FiniteAdeleRing : Type _ :=
Πʳ v : HeightOneSpectrum R, [v.adicCompletion K, v.adicCompletionIntegers K]
