theorem SylowTheorems.sylow_theorems (G : Type u_1) [Group G] [Fintype G] (p : ℕ) [Fact (Nat.Prime p)] : (∃ (H : Subgroup G), Nat.card ↥H = p ^ (Nat.card G).factorization p) ∧ (∀ (P Q : Sylow p G), ∃ (g : G), ↑P = Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) ↑Q) ∧ (∀ (K : Subgroup G), IsPGroup p ↥K → ∀ (Q : Sylow p G), ∃ (g : G), K ≤ Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) ↑Q) ∧ Nat.card (Sylow p G) ∣ Nat.card G / p ^ (Nat.card G).factorization p ∧ Nat.card (Sylow p G) ≡ 1 [MOD p]

def SylowTheorems.IsSylowPSubgroup (p : ℕ) [Fact (Nat.Prime p)] (G : Type u_1) [Group G] [Finite G] (H : Subgroup G) : Prop

theorem SylowTheorems.sylow_II {G : Type u_1} [Group G] [Finite G] {p : ℕ} [hp : Fact (Nat.Prime p)] (P Q : Sylow p G) : ∃ (g : G), ↑P = Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) ↑Q

theorem SylowTheorems.sylow_III (p : ℕ) (G : Type u_2) [Group G] [Fintype G] [Fact (Nat.Prime p)] : Nat.card (Sylow p G) ∣ Nat.card G / p ^ (Nat.card G).factorization p ∧ Nat.card (Sylow p G) ≡ 1 [MOD p]

theorem SylowTheorems.cauchy_theorem {G : Type u_2} [Group G] [Fintype G] (p : ℕ) [Fact (Nat.Prime p)] (hdvd : p ∣ Fintype.card G) : ∃ (x : G), orderOf x = p

theorem SylowTheorems.natCast_4_eq_neg1_zmod5 : ↑4 = -1

theorem SylowTheorems.val_sub_mod_5 (i j : ZMod 5) : (j - i).val = (4 * i.val + j.val) % 5

theorem SylowTheorems.mulEquiv_dihedralGroup_of_not_isCyclic (G : Type u_2) [Group G] [Fintype G] (hG : Fintype.card G = 10) (hnc : ¬IsCyclic G) : Nonempty (G ≃* DihedralGroup 5)

theorem SylowTheorems.groups_of_order_10_classification (G : Type u_2) [Group G] [Fintype G] (hG : Fintype.card G = 10) : Nonempty (G ≃* Multiplicative (ZMod 10)) ∨ Nonempty (G ≃* DihedralGroup 5)

theorem SylowTheorems.card_stabilizer_dvd_card {G : Type u_2} [Group G] [Fintype G] (H : Subgroup G) (U : Finset G) (hU : ∀ h ∈ H, ∀ u ∈ U, h * u ∈ U) : Nat.card ↥H ∣ U.card

def SylowTheorems.poles (G : Type u_2) (X : Type u_3) [Group G] [MulAction G X] : Set X

theorem SylowTheorems.smul_mem_poles {G : Type u_2} {X : Type u_3} [Group G] [MulAction G X] (g : G) (p : X) (hp : p ∈ poles G X) : g • p ∈ poles G X