Theorems · Theorem · number theory

NumberField.ComplexEmbedding.LiesOver.over_apply

∀ {K : Type u_3} {L : Type u_4} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (φ : L →+* ℂ) (ψ : K →+* ℂ)
  [NumberField.ComplexEmbedding.LiesOver φ ψ] {x : K}, φ ((algebraMap K L) x) = ψ x

Defined in

Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings

Cited by

0 results in Mathlib

Foundations

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

Assumes

FieldFieldAlgebraNumberField.ComplexEmbedding.LiesOver