isReal_comap_iff — Mathlib

English

Every infinite place of the base field k arises as a comap of an infinite place of K along algebraMap.

Русский

Каждое бесконечное место базового поля k возникает как обратное по алгебраическому отображению от бесконечного места K.

LaTeX

$$$ \forall w \in \text{InfinitePlace}(K), \exists w' \in \text{InfinitePlace}(k), w' .\mathrm{comap}(\mathrm{algebraMap}_{kK}) = w $$$

Lean4

theorem isReal_comap_iff (f : k ≃+* K) {w : InfinitePlace K} : IsReal (w.comap (f : k →+* K)) ↔ IsReal w := by
  rw [← mk_embedding w, comap_mk, isReal_mk_iff, isReal_mk_iff, ComplexEmbedding.isReal_comp_iff]

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