not_isComplex_iff_isReal

Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

URI: https://scilib.ai/kg/mathlib#NumberField.InfinitePlace.not_isComplex_iff_isReal

English

¬IsComplex w is equivalent to IsReal w.

Русский

¬IsComplex w эквивалентно IsReal w.

LaTeX

$$$\\\\neg IsComplex(w) \\\\iff IsReal(w).$$$

Lean4

@[simp]
theorem not_isComplex_iff_isReal {w : InfinitePlace K} : ¬IsComplex w ↔ IsReal w := by
  rw [isComplex_iff, isReal_iff, not_not]

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

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

Разделы

Аффилиация

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