nrComplexPlaces — Mathlib

English

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

Русский

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

LaTeX

$$$\mathrm{nrComplexPlaces}(K) = \#\{ w \in \mathrm{InfinitePlace}(K) : \mathrm{IsComplex}(w) \}$$$

Lean4

/-- The number of infinite complex places of the number field `K`. -/
noncomputable abbrev nrComplexPlaces :=
  card { w : InfinitePlace K // IsComplex w }

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