Theorems · Definition · number theory

NumberField.ComplexEmbedding.lift

(K : Type u_1) →
  [inst : Field K] →
    {k : Type u_2} → [inst_1 : Field k] → [inst_2 : Algebra k K] → [Algebra.IsAlgebraic k K] → (k →+* ℂ) → K →+* ℂ

A (random) lift of the complex embedding φ : k →+* ℂ to an extension K of k.

Defined in

Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings

Cited by

5 results in Mathlib

Foundations

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

Assumes

FieldFieldAlgebraAlgebra.IsAlgebraic