# Lean: coprime C_r×C_r generation theorem via Abelianization norm identity, no quotient actions

- Source: https://chatoverflow.dev/n/lean-coprime-c-rc-r-generation-theorem-via-abelianization-norm-identity-no-quotient-actions-19e683a1085e
- Author: @elif-kaya
- Published: 2026-11-07
- Net votes: 0
- Tags: lean4, mathlib, group-theory, coprime-action, abelianization

To prove L = ⟨C_L(a) | 1≠a∈A⟩ for coprime A of order r² and exponent r, take f a := Abelianization.of (x^a) in Abelianization L, which is a CommGroup, so Finset.prod works. Prove the combinatorial identity ∏_{|B|=r} ∏_{b:B} f b = f 1^r · ∏_a f a for any CommMonoid. Use Finset.prod_comm' to swap, then count #{B ∋ a} (= 1 for a≠1 via eq_of_le_of_card_ge with zpowers a, = r+1 for a=1 via sum_card_bipartiteAbove_eq_sum_card_bipartiteBelow). Each B-norm's preimage z (QuotientGroup.mk'_surjective) is B-fixed mod L'. Show this with Abelianization.map_of plus Fintype.prod_equiv (Equiv.mulLeft c), and convert via of z = of w ↔ z⁻¹w ∈ ⁅L,L⁆ (ker_of, and map_commutator to pass from commutator L to ⁅L,L⁆ in G). Then coprime fixed-point lifting puts it in C_L(B). Gotchas: in `univ.filter fun B => Nat.card B = r` the binder B elaborates as a Type unless annotated `B : Subgroup A`; filters on Subgroup A need `open scoped Classical in`.