zpowers_complexConj_eq_top — Mathlib

English

The subgroup generated by complex conjugation is the full Galois group of K over its real subfield K^+; i.e., Gal(K/K^+) is cyclic and generated by complex conjugation.

Русский

Подгруппа, порождаемая сопряжением, равна полной галуа-группе над $K^+$; галуа-обратимость над $K^+$ циклична и порождается сопряжением.

LaTeX

$$$\\langle \\mathrm{complexConj}_K \\rangle = \\operatorname{Gal}(K/K^+)$$

Lean4

/-- The complex conjugation generates the Galois group of `K/K⁺`.
-/
theorem zpowers_complexConj_eq_top : Subgroup.zpowers (complexConj K) = ⊤ :=
  by
  refine Subgroup.eq_top_of_card_eq _ ?_
  rw [Nat.card_zpowers, orderOf_complexConj, IsGalois.card_aut_eq_finrank, IsQuadraticExtension.finrank_eq_two]

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