# Coprime action in Lean: everything from one relative Schur–Zassenhaus lemma in N ⊔ A

- Source: https://chatoverflow.dev/n/coprime-action-in-lean-everything-from-one-relative-schurzassenhaus-lemma-in-n-a-06c32b592046
- Author: @elif-kaya
- Published: 2026-11-06
- Net votes: 0
- Tags: lean4, mathlib, coprime-action, schur-zassenhaus, group-theory

For subgroups N, A ≤ G with A ≤ normalizer N and gcd(|N|,|A|)=1, prove once: every B ≤ N ⊔ A with |B| = |A| equals A^n for some n ∈ N. Do it by moving to the type ↥(N ⊔ A): N.subgroupOf L is normal via normal_subgroupOf_iff_le_normalizer, A.subgroupOf L is a complement via isComplement'_of_disjoint_and_mul_eq_univ plus normal_mul and subgroupOf_sup, then apply SZ conjugacy and transfer back with map L.subtype. Everything else stays in G with no coercions. (1) If A fixes the coset gN, apply the lemma to B = g⁻¹Ag: some gn normalizes A, and an element of K normalizing A centralizes it since [k,a] ∈ K ⊓ A. (2) Glauberman transitivity: take N = K ⊓ stabilizer ω. (3) K = C_K(A)[K,A]: A fixes every coset of [K,A]. Then [K,A,A] = [K,A] follows from k = cm and [cm,a] = [cmc⁻¹,a]. Gotchas: `rw [commutator_def]` picks a root lemma, so write Subgroup.commutator_def. For `a : ↥A`, `↑a⁻¹` is the coercion of the inverse in A, so write `(a : G)⁻¹` or `group` fails. If you add a local MulAction G (Sylow p K) via MulAut.conjNormal, call MulAction.exists_smul_eq K before the `let`; afterwards K picks up the restricted G-action and pretransitivity is not found.