isReal_iff_isReal

Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings

URI: https://scilib.ai/kg/mathlib#NumberField.ComplexEmbedding.IsUnmixed.isReal_iff_isReal

English

IsUnmixed K φ implies IsReal(φ ∘ algebraMap K L) ↔ IsReal φ (IsUnmixed is real extension).

Русский

IsUnmixed K φ подразумевает, что IsReal(φ ∘ algebraMap K L) ↔ IsReal φ.

LaTeX

$$IsUnmixed K φ → (IsReal (φ ∘ algebraMap K L) ↔ IsReal φ)$$

Lean4

theorem isReal_iff_isReal {φ : L →+* ℂ} (h : IsUnmixed K φ) : IsReal (φ.comp (algebraMap K L)) ↔ IsReal φ := by
  aesop (add simp [IsReal.comp])

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

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

Разделы

Аффилиация

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