Complex conjugation generates the real Galois group

Mathlib classifies real algebra homomorphisms of ℂ as the identity or conjugation. Here that classification is expressed as the generator condition used by cyclic group cohomology. The quadratic-extension instance makes the Galois structure of ℂ/ℝ available to that API.

instance TauCeti.instIsQuadraticExtensionRealComplex : Algebra.IsQuadraticExtension ℝ ℂ

The complex numbers form a quadratic extension of the reals.

@[simp]

theorem TauCeti.zpowers_conjAe_eq_top : Subgroup.zpowers Complex.conjAe = ⊤

Complex conjugation generates the full group of real algebra automorphisms of ℂ.