isComplex_mk_iff

Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

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

English

IsComplex(mk φ) iff not ComplexEmbedding.IsReal φ.

Русский

IsComplex(mk φ) эквивалентно не Real φ.

LaTeX

$$$IsComplex(\\\\mathrm{mk} \\\\varphi) \\\\iff \\\\neg \\\\mathrm{ComplexEmbedding.IsReal}(\\\\varphi).$$$

Lean4

theorem isComplex_mk_iff {φ : K →+* ℂ} : IsComplex (mk φ) ↔ ¬ComplexEmbedding.IsReal φ :=
  not_isReal_iff_isComplex.symm.trans isReal_mk_iff.not

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

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

Разделы

Аффилиация

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