feat(group_theory/sylow): the cardinality of a sylow group (#11776)

Co-authored-by: tb65536 <tb65536@users.noreply.github.com>

Author: nomeata

src/algebra/is_prime_pow.lean

@@ -182,9 +182,9 @@ begin
     simp [hab, finset.filter_singleton, not_is_prime_pow_one] },
   refine ⟨_, λ h, or.elim h (λ i, i.trans (dvd_mul_right _ _)) (λ i, i.trans (dvd_mul_left _ _))⟩,
   obtain ⟨p, k, hp, hk, rfl⟩ := (is_prime_pow_nat_iff _).1 hn,
-  simp only [nat.prime_pow_dvd_iff_le_factorization _ _ _ hp (mul_ne_zero ha hb),
-    nat.factorization_mul ha hb, nat.prime_pow_dvd_iff_le_factorization _ _ _ hp ha,
-    nat.prime_pow_dvd_iff_le_factorization _ _ _ hp hb, pi.add_apply, finsupp.coe_add],
+  simp only [hp.pow_dvd_iff_le_factorization (mul_ne_zero ha hb),
+    nat.factorization_mul ha hb, hp.pow_dvd_iff_le_factorization ha,
+    hp.pow_dvd_iff_le_factorization hb, pi.add_apply, finsupp.coe_add],
   have : a.factorization p = 0 ∨ b.factorization p = 0,
   { rw [←finsupp.not_mem_support_iff, ←finsupp.not_mem_support_iff, ←not_and_distrib,
       ←finset.mem_inter],

src/data/nat/factorization.lean

@@ -199,10 +199,14 @@ begin
   { rintro ⟨c, rfl⟩, rw factorization_mul hd (right_ne_zero_of_mul hn), simp },
 end
 
-lemma prime_pow_dvd_iff_le_factorization (p k n : ℕ) (pp : prime p) (hn : n ≠ 0) :
+lemma prime.pow_dvd_iff_le_factorization {p k n : ℕ} (pp : prime p) (hn : n ≠ 0) :
   p ^ k ∣ n ↔ k ≤ n.factorization p :=
 by rw [←factorization_le_iff_dvd (pow_pos pp.pos k).ne' hn, pp.factorization_pow, single_le_iff]
 
+lemma prime.pow_dvd_iff_dvd_pow_factorization {p k n : ℕ} (pp : prime p) (hn : n ≠ 0) :
+  p ^ k ∣ n ↔ p ^ k ∣ p ^ n.factorization p :=
+by rw [pow_dvd_pow_iff_le_right pp.one_lt, pp.pow_dvd_iff_le_factorization hn]
+
 lemma exists_factorization_lt_of_lt {a b : ℕ} (ha : a ≠ 0) (hab : a < b) :
   ∃ p : ℕ, a.factorization p < b.factorization p :=
 begin
@@ -241,7 +245,7 @@ lemma pow_factorization_dvd (p d : ℕ) : p ^ d.factorization p ∣ d :=
 begin
   rcases eq_or_ne d 0 with rfl | hd, { simp },
   by_cases pp : prime p,
-  { rw prime_pow_dvd_iff_le_factorization p _ d pp hd },
+  { rw pp.pow_dvd_iff_le_factorization hd },
   { rw factorization_eq_zero_of_non_prime d p pp, simp },
 end
 
@@ -255,7 +259,7 @@ begin
     intros p,
     by_cases pp : prime p, swap,
     { rw factorization_eq_zero_of_non_prime d p pp, exact zero_le' },
-    rw ←prime_pow_dvd_iff_le_factorization p _ n pp hn,
+    rw ←pp.pow_dvd_iff_le_factorization hn,
     exact h p _ pp (pow_factorization_dvd p _) },
 end
 

src/group_theory/sylow.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes, Thomas Browning
 -/
 
+import data.nat.factorization
 import data.set_like.fintype
 import group_theory.group_action.conj_act
 import group_theory.p_group
@@ -467,6 +468,17 @@ begin
   rwa [h, card_bot] at key,
 end
 
+/-- The cardinality of a Sylow group is `p ^ n`
+ where `n` is the multiplicity of `p` in the group order. -/
+lemma card_eq_multiplicity [fintype G] {p : ℕ} [hp : fact p.prime] (P : sylow p G) :
+  card P = p ^ nat.factorization (card G) p :=
+begin
+  obtain ⟨n, heq : card P = _⟩ := is_p_group.iff_card.mp (P.is_p_group'),
+  refine nat.dvd_antisymm _ (P.pow_dvd_card_of_pow_dvd_card (nat.pow_factorization_dvd p _)),
+  rw [heq, ←hp.out.pow_dvd_iff_dvd_pow_factorization (show card G ≠ 0, from card_ne_zero), ←heq],
+  exact P.1.card_subgroup_dvd_card,
+end
+
 lemma subsingleton_of_normal {p : ℕ} [fact p.prime] [fintype (sylow p G)] (P : sylow p G)
   (h : (P : subgroup G).normal) : subsingleton (sylow p G) :=
 begin