Theorems · Theorem · number theory

NumberField.ComplexEmbedding.IsConj.isReal_comp

∀ {K : Type u_1} [inst : Field K] {k : Type u_2} [inst_1 : Field k] [inst_2 : Algebra k K] {φ : K →+* ℂ} {σ : Gal(K/k)},
  NumberField.ComplexEmbedding.IsConj φ σ → NumberField.ComplexEmbedding.IsReal (φ.comp (algebraMap k K))

Defined in

Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings

Cited by

2 results in Mathlib

Foundations

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

Assumes

FieldFieldAlgebra