nrComplexPlaces_eq_zero — Mathlib

English

If a number field K is totally real, then there are no complex places: the number of complex places nrComplexPlaces(K) is zero.

Русский

Если число поле K полностью вещественное, то комплексные места отсутствуют: nrComplexPlaces(K) = 0.

LaTeX

$$$\text{IsTotallyReal}(K) \implies \operatorname{nrComplexPlaces}(K) = 0$$$

Lean4

@[simp]
theorem nrComplexPlaces_eq_zero [h : IsTotallyReal K] : nrComplexPlaces K = 0 :=
  nrComplexPlaces_eq_zero_iff.mpr h

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