nrRealPlaces_eq_zero

Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex

URI: https://scilib.ai/kg/mathlib#NumberField.IsTotallyComplex.nrRealPlaces_eq_zero

English

If K is totally complex, then nrRealPlaces(K) = 0.

Русский

Если K полностью комплексно, то nrRealPlaces(K) = 0.

LaTeX

$$$\text{IsTotallyComplex}(K) \Rightarrow \ operatorname{nrRealPlaces}(K) = 0$$$

Lean4

@[simp]
theorem nrRealPlaces_eq_zero [h : IsTotallyComplex K] : nrRealPlaces K = 0 :=
  nrRealPlaces_eq_zero_iff.mpr h

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

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

Разделы

Аффилиация

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