eq_of_embedding_eq_conjugate — Mathlib

English

Let K be a field and v1, v2 be infinite places of K. If the embedding associated to v1 is the complex conjugate of the embedding associated to v2, then v1 = v2.

Русский

Пусть K — поле, возьмём две бесконечных места v1 и v2 над K. Если соответствующее v1 вложение равно конъюгированному вложению v2, то v1 = v2.

LaTeX

$$$\\\\forall v_1,v_2 \\\\in \\\\mathrm{InfinitePlace}(K),\\\\; \\mathrm{embedding}(v_1) = \\mathrm{ComplexEmbedding}.\\\\mathrm{conjugate}(\\\\mathrm{embedding}(v_2)) \\\\Rightarrow v_1 = v_2.$$$

Lean4

theorem eq_of_embedding_eq_conjugate {v₁ v₂ : InfinitePlace K}
    (h : v₁.embedding = ComplexEmbedding.conjugate v₂.embedding) : v₁ = v₂ := by
  rw [← mk_embedding v₁, h, mk_conjugate_eq, mk_embedding]

Похожие утверждения