Theorems · Theorem · number theory

NumberField.ComplexEmbedding.IsConj.eq

∀ {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 φ σ → ∀ (x : K), φ (σ x) = star (φ x)

Defined in

Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings

Cited by

5 results in Mathlib

Foundations

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

Assumes

FieldFieldAlgebra