infinitePlace_complexConj — Mathlib

English

The complex conjugation automorphism is not the identity; it is a nontrivial automorphism of the CM-field fixing K⁺.

Русский

Сопряжение не равно тождественному отображению; это не тривиальный автоморфизм CM‑поля, фиксирующий K⁺.

LaTeX

$$complexConj K ≠ 1_K$$

Lean4

@[simp]
theorem infinitePlace_complexConj (w : InfinitePlace K) (x : K) : w (complexConj K x) = w x := by
  rw [← norm_embedding_eq, complexEmbedding_complexConj, Complex.norm_conj, norm_embedding_eq]

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