Theorems · Definition · number theory

NumberField.mixedEmbedding.indexEquiv

(K : Type u_1) → [inst : Field K] → [NumberField K] → NumberField.mixedEmbedding.index K ≃ (K →+* ℂ)

The Equiv between index K and K →+* ℂ defined by sending a real infinite place w to the unique corresponding embedding w.embedding, and the pair ⟨w, 0⟩ (resp. ⟨w, 1⟩) for a complex infinite place w to w.embedding (resp. conjugate w.embedding).

Defined in

Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Cited by

6 results in Mathlib

Foundations

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

Assumes

FieldNumberField