conjugate_comp_ne

Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings

URI: https://scilib.ai/kg/mathlib#NumberField.ComplexEmbedding.Extension.conjugate_comp_ne

English

If φ is an extension of ψ and ¬IsReal ψ, then ¬IsReal φ.

Русский

Если φ — расширение ψ и не является реальным ψ, то φ не реален.

LaTeX

$$¬IsReal(ψ) → ¬IsReal(φ.1)$$

Lean4

theorem conjugate_comp_ne (h : ¬IsReal ψ) : (conjugate φ).comp (algebraMap K L) ≠ ψ := by
  simp_all [ComplexEmbedding.isReal_iff, comp_eq]

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

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

Разделы

Аффилиация

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