The order of the p-power classes of a finite commutative group

Let G be a finite commutative group and p a prime. Once p ^ m contains the full power of p dividing #G, the p ^ m-th power map kills exactly the Sylow p-subgroup of G, so the power class group G ⧸ G^(p^m) has the order of that Sylow subgroup. It is the maximal p-quotient of G, and it no longer depends on m.

Main results

• TauCeti.natCard_powerClassQuotient_prime_pow: #(G ⧸ G^(p^m)) = p ^ v_p(#G) whenever v_p(#G) ≤ m.

theorem TauCeti.natCard_powerClassQuotient_prime_pow (G : Type u_1) [CommGroup G] [Finite G] {p : ℕ} [Fact (Nat.Prime p)] {m : ℕ} (hm : (Nat.card G).factorization p ≤ m) : Nat.card (powerClassQuotient G (p ^ m)) = p ^ (Nat.card G).factorization p

The p-power classes of a finite commutative group. If p ^ m contains the full power of p dividing #G, then G ⧸ G^(p^m) has order that power of p, the order of a Sylow p-subgroup of G.