indexEquiv_apply_isComplex_fst — Mathlib

English

Let w be a complex place of K. Then the index map sends Sum.inr ⟨w, 0⟩ to the complex embedding corresponding to w.

Русский

Пусть w — комплексное место поля K. Тогда отображение индекса отправляет Sum.inr ⟨w, 0⟩ в встраивание, соответствующее w.

LaTeX

$$$ (indexEquiv K) (Sum.inr \langle w, 0 \rangle) = w.val.embedding $$$

Lean4

@[simp]
theorem indexEquiv_apply_isComplex_fst (w : { w : InfinitePlace K // IsComplex w }) :
    (indexEquiv K) (Sum.inr ⟨w, 0⟩) = w.val.embedding :=
  rfl

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