indexEquiv_apply_isComplex_snd — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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