Theorems · Definition · number theory

IsDedekindDomain.FiniteAdeleRing.algebraMap

(R : Type u_1) →
  [inst : CommRing R] →
    [inst_1 : IsDedekindDomain R] →
      (K : Type u_2) →
        [inst_2 : Field K] →
          [inst_3 : Algebra R K] → [inst_4 : IsFractionRing R K] → K →+* IsDedekindDomain.FiniteAdeleRing R K

The canonical map from K to the finite adeles of K. The content of the existence of this map is the fact that an element k of K is integral at all but finitely many places, which is IsDedekindDomain.HeightOneSpectrum.Support.finite R k.

Defined in

Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommRingIsDedekindDomainFieldAlgebraIsFractionRing