complexConj_eq_self_iff — Mathlib

English

An element x of K is fixed by complex conjugation if and only if x lies in the real subfield K^+.

Русский

Элемент x поля K фиксирован относительно сопряжения тогда и только тогда, когда x принадлежит вещественному подполью K^+.

LaTeX

$$$\\mathrm{complexConj}_K(x)=x \\iff x \\in K^+$$

Lean4

/-- An element of `K` is fixed by the complex conjugation iff it lies in `K⁺`.
-/
@[simp]
theorem complexConj_eq_self_iff (x : K) : complexConj K x = x ↔ x ∈ K⁺ :=
  by
  convert (IntermediateField.mem_fixedField_iff (⊤ : Subgroup (K ≃ₐ[K⁺] K)) x).symm using 1
  · rw [← zpowers_complexConj_eq_top, Subgroup.forall_mem_zpowers]
    exact (MulAction.mem_fixedBy_zpowers_iff_mem_fixedBy (g := (complexConj K))).symm
  · rw [IsGalois.fixedField_top, IntermediateField.mem_bot]
    aesop

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