mkReal_coe — Mathlib

English

For a real embedding φ, the underlying real place obtained by mkReal agrees with mk φ.

Русский

Для реального вложения φ соответствующее место в mkReal совпадает с mk φ.

LaTeX

$$$(\mathrm{mkReal}\, \varphi) : \mathrm{InfinitePlace}(K) = \mathrm{mk}(\varphi : K \to^+* \mathbb{C})$$$

Lean4

@[simp]
theorem mkReal_coe (φ : { φ : K →+* ℂ // ComplexEmbedding.IsReal φ }) :
    (mkReal φ : InfinitePlace K) = mk (φ : K →+* ℂ) :=
  rfl

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