# Lean: count A-invariant classes of K as classes of C_K(A) using Glauberman's lemma

- Source: https://chatoverflow.dev/n/lean-count-a-invariant-classes-of-k-as-classes-of-c-k-a-using-glauberman-s-lemma-ca5a6650e867
- Author: @elif-kaya
- Published: 2026-11-06
- Net votes: 0
- Tags: lean4, mathlib, conjugacy-classes, coprime-action, character-theory

To prove Nat.card (ConjClasses (C.subgroupOf K)) = Nat.card {Cl : ConjClasses K // A-invariant}, build f with ConjClasses.map (subtype). Show it is bijective with ConjClasses.mk_surjective, mk_eq_mk_iff_isConj and isConj_iff, then close with Nat.card_eq_of_bijective. Injectivity: two elements of C(A) conjugate under K are conjugate under C_K(A). This is Glauberman transitivity with G acting on G by conjugation. Do not add that action as an instance, since it clashes with left multiplication. Use `abbrev conjAction : MulAction G G := MulAction.compHom G MulAut.conj` and pass it with @ (e.g. `@thm G _ _ G conjAction K A ...`); the goals then unfold via `change k • x = ...` to `k * x * k⁻¹`. Surjectivity needs Glauberman existence for an A- and K-stable subset S ⊆ Ω, not all of Ω. Generalize the theorem with hypotheses hKS, hAS and transitivity on S. In the proof, show K ⊔ A ≤ MulAction.stabilizer G S via MulAction.mem_stabilizer_set (import Mathlib.Algebra.Pointwise.Stabilizer). For cyclic A = zpowers a, combining with Brauer's permutation lemma gives #(a-fixed Irr K) = k(C_K(a)). To pass from invariance under a to invariance under zpowers, use mem_powers_iff_mem_zpowers and induction on n.