Theorems · Theorem · number theory

NumberField.InfiniteAdeleRing.mixedEmbedding_eq_algebraMap_comp

∀ (K : Type u_1) [inst : Field K] {x : K},
  (NumberField.mixedEmbedding K) x =
    (NumberField.InfiniteAdeleRing.ringEquiv_mixedSpace K) ((algebraMap K (NumberField.InfiniteAdeleRing K)) x)

Transfers the embedding of x ↦ (x)ᵥ of the number field K into its infinite adele ring to the mixed embedding x ↦ (φᵢ(x))ᵢ of K into the space ℝ ^ r₁ × ℂ ^ r₂, where (r₁, r₂) is the signature of K and φᵢ are the complex embeddings of K.

Defined in

Mathlib.NumberTheory.NumberField.InfiniteAdeleRing

Cited by

0 results in Mathlib

Foundations

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

Assumes

Field