nrRealPlaces — Mathlib

English

Let K be a number field. The quantity nrRealPlaces(K) equals the cardinality of the set of real infinite places of K.

Русский

Пусть K — числовое поле. Число nrRealPlaces(K) равно кардиналу множества вещественных бесконечных мест поля K.

LaTeX

$$$\mathrm{nrRealPlaces}(K) = \#\{ w \in \mathrm{InfinitePlace}(K) : \mathrm{IsReal}(w) \}$$$

Lean4

/-- The number of infinite real places of the number field `K`. -/
noncomputable abbrev nrRealPlaces :=
  card { w : InfinitePlace K // IsReal w }

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