feat(group_theory/exponent): card G ∣ exponent G ^ rank G (#16354)

This PR adds a lemma stating that `nat.card G ∣ monoid.exponent G ^ group.rank G`.

src/group_theory/exponent.lean

@@ -3,6 +3,8 @@ Copyright (c) 2021 Julian Kuelshammer. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Julian Kuelshammer
 -/
+import data.zmod.quotient
+import group_theory.noncomm_pi_coprod
 import group_theory.order_of_element
 import algebra.gcd_monoid.finset
 import algebra.punit_instances
@@ -313,3 +315,32 @@ end
 end cancel_comm_monoid
 
 end monoid
+
+section comm_group
+
+open subgroup
+open_locale big_operators
+
+variables (G) [comm_group G] [group.fg G]
+
+@[to_additive] lemma card_dvd_exponent_pow_rank : nat.card G ∣ monoid.exponent G ^ group.rank G :=
+begin
+  obtain ⟨S, hS1, hS2⟩ := group.rank_spec G,
+  rw [←hS1, ←fintype.card_coe, ←finset.card_univ, ←finset.prod_const],
+  let f : (Π g : S, zpowers (g : G)) →* G := noncomm_pi_coprod (λ s t h x y hx hy, mul_comm x y),
+  have hf : function.surjective f,
+  { rw [←monoid_hom.range_top_iff_surjective, eq_top_iff, ←hS2, closure_le],
+    exact λ g hg, ⟨pi.mul_single ⟨g, hg⟩ ⟨g, mem_zpowers g⟩, noncomm_pi_coprod_mul_single _ _⟩ },
+  replace hf := nat_card_dvd_of_surjective f hf,
+  rw nat.card_pi at hf,
+  refine hf.trans (finset.prod_dvd_prod_of_dvd _ _ (λ g hg, _)),
+  rw ← order_eq_card_zpowers',
+  exact monoid.order_dvd_exponent (g : G),
+end
+
+@[to_additive] lemma card_dvd_exponent_pow_rank' {n : ℕ} (hG : ∀ g : G, g ^ n = 1) :
+  nat.card G ∣ n ^ group.rank G :=
+(card_dvd_exponent_pow_rank G).trans
+    (pow_dvd_pow_of_dvd (monoid.exponent_dvd_of_forall_pow_eq_one G n hG) (group.rank G))
+
+end comm_group