theorem NumberField.InfinitePlace.embedding_injective (K : Type u_1) [Field K] : Function.Injective fun (v : InfinitePlace K) => v.embedding

theorem NumberField.InfinitePlace.conjugate_embedding_injective (K : Type u_1) [Field K] : Function.Injective fun (v : InfinitePlace K) => ComplexEmbedding.conjugate v.embedding

theorem NumberField.InfinitePlace.eq_of_embedding_eq_conjugate (K : Type u_1) [Field K] {v₁ v₂ : InfinitePlace K} (h : v₁.embedding = ComplexEmbedding.conjugate v₂.embedding) : v₁ = v₂