eq

Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings

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

English

If φ is conjugated by σ, then φ(σ x) equals the complex conjugate of φ(x) for all x.

Русский

Если φ конъюгировано σ, то φ(σ x) равно сопряжённому к φ(x) для всех x.

LaTeX

$$$\forall x,\; φ(σ(x)) = \overline{φ(x)}$$$

Lean4

theorem eq (h : IsConj φ σ) (x) : φ (σ x) = star (φ x) :=
  RingHom.congr_fun h.symm x

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

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

Разделы

Аффилиация

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