From ac49df8144e602e3eb5c0e5eaa042ddb78f6a263 Mon Sep 17 00:00:00 2001
From: Thomas Browning <tb65536@uw.edu>
Date: Tue, 27 Sep 2022 11:53:00 +0000
Subject: [PATCH] =?UTF-8?q?feat(group=5Ftheory/exponent):=20`card=20G=20?=
 =?UTF-8?q?=E2=88=A3=20exponent=20G=20^=20rank=20G`=20(#16354)?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This PR adds a lemma stating that `nat.card G ∣ monoid.exponent G ^ group.rank G`.
---
 src/group_theory/exponent.lean | 31 +++++++++++++++++++++++++++++++
 1 file changed, 31 insertions(+)

diff --git a/src/group_theory/exponent.lean b/src/group_theory/exponent.lean
index b7a8183ec2526..02da4ee73ae32 100644
--- a/src/group_theory/exponent.lean
+++ b/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