isConj_apply_apply

Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings

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

English

If hσ: IsConj φ σ, then σ(σ x) = x for all x in K.

Русский

Если hσ: IsConj φ σ, тогда для всех x в K выполняется σ(σ x) = x.

LaTeX

$$IsConj φ σ → ∀ x, σ(σ x) = x$$

Lean4

theorem isConj_apply_apply (hσ : IsConj φ σ) (x : K) : σ (σ x) = x := by simp [← φ.injective.eq_iff, hσ.eq]

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

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

Разделы

Аффилиация

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