conjugate_embedding_injective — Mathlib

English

The map sending an infinite place to the complex conjugate of its embedding is injective.

Русский

Отображение, отправляющее бесконечное место в сопряжённое вложение, инъективно.

LaTeX

$$conjugate_embedding_injective$$

Lean4

theorem conjugate_embedding_injective :
    (fun (v : InfinitePlace K) ↦ ComplexEmbedding.conjugate v.embedding).Injective :=
  star_injective.comp <| embedding_injective K

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