Theorems · Definition · number theory

IsDedekindDomain.FiniteAdeleRing

(R : Type u_1) →
  [inst : CommRing R] →
    [IsDedekindDomain R] →
      (K : Type u_2) → [inst_2 : Field K] → [inst_3 : Algebra R K] → [IsFractionRing R K] → Type (max u_2 u_1)

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.

Defined in

Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing

Cited by

9 results in Mathlib

Foundations

Depth 183 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingIsDedekindDomainFieldAlgebraIsFractionRing