nrComplexPlaces_eq_zero_iff

Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex

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

← MathLib Explorer

English

A number field K is totally real if and only if nrComplexPlaces(K) = 0.

Русский

Числовое поле K полностью вещественное тогда и только тогда, когда nrComplexPlaces(K) = 0.

LaTeX

$$nrComplexPlaces(K) = 0 \\iff IsTotallyReal(K).$$

Lean4

theorem nrComplexPlaces_eq_zero_iff : nrComplexPlaces K = 0 ↔ IsTotallyReal K := by
  simp [Fintype.card_eq_zero_iff, isEmpty_subtype, isTotallyReal_iff]

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

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

Разделы

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

Аффилиация

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