conjugate_comp

Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings

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

English

The conjugate of a composed embedding equals the composition of conjugates.

Русский

Сопряжение композиции вложений равно композиции сопряжений.

LaTeX

$$(conjugate φ) ∘ σ = conjugate (φ ∘ σ)$$

Lean4

@[simp]
theorem conjugate_comp (φ : K →+* ℂ) (σ : k →+* K) : (conjugate φ).comp σ = conjugate (φ.comp σ) :=
  rfl

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

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

Разделы

Аффилиация

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