mkComplex_coe

Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

URI: https://scilib.ai/kg/mathlib#NumberField.InfinitePlace.mkComplex_coe

English

The number of real embeddings equals nrRealPlaces(K).

Русский

Число реальных вложений равно nrRealPlaces(K).

LaTeX

$$$\#\{ \varphi : K \to \mathbb{C} \mid \mathrm{ComplexEmbedding.IsReal}(\varphi) \} = \mathrm{nrRealPlaces}(K)$$$

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru