Theorems · Definition · number theory

NumberField.AdeleRing

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

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.

Defined in

Mathlib.NumberTheory.NumberField.AdeleRing

Cited by

3 results in Mathlib

Foundations

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

Assumes

CommRingIsDedekindDomainFieldAlgebraIsFractionRing