conjugate_embedding_eq_of_isReal — Mathlib

English

If w is real, then ComplexEmbedding.conjugate (embedding w) = embedding w.

Русский

Если w реальное, то ComplexEmbedding.conjugate (embedding w) = embedding w.

LaTeX

$$$\\text{conjugateEmbedding}(w) = \\mathrm{ComplexEmbedding}.\\mathrm{conjugate}(\\mathrm{embedding}(w)) = \\mathrm{embedding}(w).$$$

Lean4

@[simp]
theorem conjugate_embedding_eq_of_isReal {w : InfinitePlace K} (h : IsReal w) :
    ComplexEmbedding.conjugate (embedding w) = embedding w :=
  ComplexEmbedding.isReal_iff.mpr (isReal_iff.mp h)

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