comp

Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings

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

← MathLib Explorer

English

For hσ: IsConj φ σ and any ν: K ≃ₐ[k] K, IsConj (φ ∘ ν) (ν⁻¹ * σ * ν).

Русский

Для hσ: IsConj φ σ и любого ν: K ≃ₐ[k] K, IsConj (φ ∘ ν) (ν⁻¹ · σ · ν).

LaTeX

$$IsConj φ σ → IsConj (φ ∘ ν) (ν⁻¹ * σ * ν)$$

Lean4

theorem comp (hσ : IsConj φ σ) (ν : K ≃ₐ[k] K) : IsConj (φ.comp ν) (ν⁻¹ * σ * ν) :=
  by
  ext
  simpa [← AlgEquiv.mul_apply, ← mul_assoc] using RingHom.congr_fun hσ _

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

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

Разделы

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

Аффилиация

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