nrRealPlaces_eq_zero_iff

Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex

URI: https://scilib.ai/kg/mathlib#NumberField.nrRealPlaces_eq_zero_iff

← MathLib Explorer

English

The field K has nrRealPlaces(K) = 0 if and only if K is totally complex.

Русский

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

LaTeX

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

Lean4

theorem nrRealPlaces_eq_zero_iff : nrRealPlaces K = 0 ↔ IsTotallyComplex K := by
  simp [Fintype.card_eq_zero_iff, isEmpty_subtype, isTotallyComplex_iff]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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