complexConj_apply_eq_self — Mathlib

English

In a CM field K, the complex conjugation fixes every element of the maximal real subfield K^+. Specifically, for all x in K^+, complexConj_K(x) = x.

Русский

В CM-поле K комплексное сопряжение фиксирует каждое элемент $x$ из максимального вещественного подполя $K^+$. Пусть $x \\in K^+$, тогда complexConj_K(x) = x.

LaTeX

$$$\\\\forall x \\,\\\\in \\\\;K^+:\\; \\\\mathrm{complexConj}_K(x)=x$$$

Lean4

@[simp]
theorem complexConj_apply_eq_self (x : K⁺) : complexConj K x = x :=
  AlgEquiv.commutes _ x

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