Mathlib Map

Theorems · Definition · number theory

IsDedekindDomain.FiniteAdeleRing.unitEmbedding

(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 global embedding of the units of K into the units of FiniteAdeleRing R K.

Defined in
Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing
Cited by
1 results in Mathlib
Foundations
Depth 195 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
CommRingIsDedekindDomainFieldAlgebraIsFractionRing
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

IsDedekindDomain.FiniteAdeleRing.unitEmbedding_apply · cited by 0FiniteAdeleRing.unitEmbed…CommRing · cited by 17173CommRingAlgebra · cited by 11388AlgebraField · cited by 7404FieldAlgebra.algebraMap · cited by 4706Algebra.algebraMapMonoidHom · cited by 3629MonoidHomUnits · cited by 2804UnitsIsFractionRing · cited by 738IsFractionRingIsDedekindDomain · cited by 668IsDedekindDomainMonoidHomClass.toMonoidHom · cited by 294MonoidHomClass.toMonoidHomUnits.map · cited by 95Units.mapIsDedekindDomain.FiniteAdeleRing · cited by 9IsDedekindDomain.FiniteAd…FiniteAdeleRing.unitEmbeddingCITED BYCITES

Cites11

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by1

Results whose statement or proof uses this declaration.