isReal_of_mk_isReal

Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

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

← MathLib Explorer

English

If IsReal (mk φ) then ComplexEmbedding.IsReal φ.

Русский

Если IsReal (mk φ), то ComplexEmbedding.IsReal φ.

LaTeX

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

Lean4

@[simp]
theorem isReal_of_mk_isReal {φ : K →+* ℂ} (h : IsReal (mk φ)) : ComplexEmbedding.IsReal φ :=
  by
  contrapose! h
  rw [not_isReal_iff_isComplex]
  exact ⟨φ, h, rfl⟩

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

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

Разделы

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

Аффилиация

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