Theorems · Theorem · number theory

NumberField.ComplexEmbedding.exists_comp_symm_eq_of_comp_eq

∀ {K : Type u_1} [inst : Field K] {k : Type u_2} [inst_1 : Field k] [inst_2 : Algebra k K] [IsGalois k K]
  (φ ψ : K →+* ℂ), φ.comp (algebraMap k K) = ψ.comp (algebraMap k K) → ∃ σ, φ.comp ↑σ.symm = ψ

Defined in

Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings

Cited by

1 results in Mathlib

Foundations

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

Assumes

FieldFieldAlgebraIsGalois