isReal_mk_iff

Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

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

English

IsReal(mk φ) is equivalent to ComplexEmbedding.IsReal φ.

Русский

IsReal(mk φ) эквивалентно ComplexEmbedding.IsReal φ.

LaTeX

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

Lean4

theorem isReal_mk_iff {φ : K →+* ℂ} : IsReal (mk φ) ↔ ComplexEmbedding.IsReal φ :=
  ⟨isReal_of_mk_isReal, fun H ↦ ⟨_, H, rfl⟩⟩

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

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

Разделы

Аффилиация

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