Theorems · Definition · number theory

NumberField.ComplexEmbedding.IsUnmixed

(K : Type u_3) → {L : Type u_4} → [inst : Field K] → [inst_1 : Field L] → [Algebra K L] → (L →+* ℂ) → Prop

If L/K and φ : L →+* ℂ, then IsMixed K φ if φ is not mixed in K, i.e., φ is real if and only if it's restriction to K is. This is the complex embedding analogue of InfinitePlace.IsUnramified K w, where w : InfinitePlace L. In this case there is an isomorphism between unmixed embeddings and unramified infinite places.

Defined in

Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings

Cited by

5 results in Mathlib

Foundations

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

Assumes

FieldFieldAlgebra