card_real_embeddings — Mathlib

English

Let K be a field with a number field structure. Then the number of real embeddings of K into the complex numbers equals nrRealPlaces K.

Русский

Пусть K имеет структуру числа поля. Тогда число действительных вложений K в комплексные числа равно nrRealPlaces K.

LaTeX

$$$\left| \{ \varphi: K \to \mathbb{C} \mid \operatorname{IsReal}(\varphi) \} \right| = nrRealPlaces(K).$$$

Lean4

theorem card_real_embeddings : card { φ : K →+* ℂ // ComplexEmbedding.IsReal φ } = nrRealPlaces K :=
  Fintype.card_congr mkReal

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