lift_algebraMap_apply

Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings

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

← MathLib Explorer

English

The conjugate of a complex embedding φ: K →+* ℂ is another embedding star φ: K →+* ℂ.

Русский

Сопряжение вложения φ: K →+* ℂ给ёт другое вложение star φ: K →+* ℂ.

LaTeX

$$conjugate (φ) := star φ$$

Lean4

@[simp]
theorem lift_algebraMap_apply [Algebra k K] [Algebra.IsAlgebraic k K] (φ : k →+* ℂ) (x : k) :
    lift K φ (algebraMap k K x) = φ x :=
  RingHom.congr_fun (lift_comp_algebraMap K φ) x

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

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

Разделы

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

Аффилиация

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