Theorems · Inductive type · number theory

NumberField.ComplexEmbedding.LiesOver

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

If L/K, ψ : K →+* ℂ, and φ : L →+* ℂ, then φ lies over ψ if the restriction of φ to K is ψ.

Defined in

Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings

Cited by

19 results in Mathlib

Foundations

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

Assumes

FieldFieldAlgebra