Sylow theorems #

The Sylow theorems are the following results for every finite group G and every prime number p.

There exists a Sylow p-subgroup of G.
All Sylow p-subgroups of G are conjugate to each other.
Let nₚ be the number of Sylow p-subgroups of G, then nₚ divides the index of the Sylow p-subgroup, nₚ ≡ 1 [MOD p], and nₚ is equal to the index of the normalizer of the Sylow p-subgroup in G.

Main definitions #

sylow p G : The type of Sylow p-subgroups of G.

Main statements #

exists_subgroup_card_pow_prime: A generalization of Sylow's first theorem: For every prime power pⁿ dividing the cardinality of G, there exists a subgroup of G of order pⁿ.
is_p_group.exists_le_sylow: A generalization of Sylow's first theorem: Every p-subgroup is contained in a Sylow p-subgroup.
sylow_conjugate: A generalization of Sylow's second theorem: If the number of Sylow p-subgroups is finite, then all Sylow p-subgroups are conjugate.
card_sylow_modeq_one: A generalization of Sylow's third theorem: If the number of Sylow p-subgroups is finite, then it is congruent to 1 modulo p.

source

structure sylow (p : ℕ) (G : Type u_1) [group G] :

Type u_1

to_subgroup : subgroup G
is_p_group' : is_p_group p ↥(self.to_subgroup)
is_maximal' : ∀ {Q : subgroup G}, is_p_group p ↥Q → self.to_subgroup ≤ Q → Q = self.to_subgroup

A Sylow p-subgroup is a maximal p-subgroup.

Instances for sylow

source

@[protected, instance]

def sylow.subgroup.has_coe {p : ℕ} {G : Type u_1} [group G] :

has_coe (sylow p G) (subgroup G)

Equations

sylow.subgroup.has_coe = {coe := sylow.to_subgroup _inst_1}

source

@[simp]

theorem sylow.to_subgroup_eq_coe {p : ℕ} {G : Type u_1} [group G] {P : sylow p G} :

P.to_subgroup = ↑P

source

@[ext]

theorem sylow.ext {p : ℕ} {G : Type u_1} [group G] {P Q : sylow p G} (h : ↑P = ↑Q) :

P = Q

source

theorem sylow.ext_iff {p : ℕ} {G : Type u_1} [group G] {P Q : sylow p G} :

P = Q ↔ ↑P = ↑Q

source

@[protected, instance]

def sylow.set_like {p : ℕ} {G : Type u_1} [group G] :

set_like (sylow p G) G

Equations

sylow.set_like = {coe := coe coe_to_lift, coe_injective' := _}

source

@[protected, instance]

def sylow.subgroup_class {p : ℕ} {G : Type u_1} [group G] :

subgroup_class (sylow p G) G

Equations

sylow.subgroup_class = {to_submonoid_class := {to_mul_mem_class := {mul_mem := _}, one_mem := _}, inv_mem := _}

source

@[protected, instance]

def sylow.mul_action_left {p : ℕ} {G : Type u_1} [group G] (P : sylow p G) {α : Type u_2} [mul_action G α] :

mul_action ↥P α

The action by a Sylow subgroup is the action by the underlying group.

Equations

P.mul_action_left = ↑P.mul_action

source

def sylow.comap_of_ker_is_p_group {p : ℕ} {G : Type u_1} [group G] (P : sylow p G) {K : Type u_2} [group K] (ϕ : K →* G) (hϕ : is_p_group p ↥(ϕ.ker)) (h : ↑P ≤ ϕ.range) :

sylow p K

The preimage of a Sylow subgroup under a p-group-kernel homomorphism is a Sylow subgroup.

Equations

P.comap_of_ker_is_p_group ϕ hϕ h = {to_subgroup := {carrier := (subgroup.comap ϕ P.to_subgroup).carrier, mul_mem' := _, one_mem' := _, inv_mem' := _}, is_p_group' := _, is_maximal' := _}

source

@[simp]

theorem sylow.coe_comap_of_ker_is_p_group {p : ℕ} {G : Type u_1} [group G] (P : sylow p G) {K : Type u_2} [group K] (ϕ : K →* G) (hϕ : is_p_group p ↥(ϕ.ker)) (h : ↑P ≤ ϕ.range) :

↑(P.comap_of_ker_is_p_group ϕ hϕ h) = subgroup.comap ϕ ↑P

source

def sylow.comap_of_injective {p : ℕ} {G : Type u_1} [group G] (P : sylow p G) {K : Type u_2} [group K] (ϕ : K →* G) (hϕ : function.injective ⇑ϕ) (h : ↑P ≤ ϕ.range) :

sylow p K

The preimage of a Sylow subgroup under an injective homomorphism is a Sylow subgroup.

Equations

P.comap_of_injective ϕ hϕ h = P.comap_of_ker_is_p_group ϕ _ h

source

@[simp]

theorem sylow.coe_comap_of_injective {p : ℕ} {G : Type u_1} [group G] (P : sylow p G) {K : Type u_2} [group K] (ϕ : K →* G) (hϕ : function.injective ⇑ϕ) (h : ↑P ≤ ϕ.range) :

↑(P.comap_of_injective ϕ hϕ h) = subgroup.comap ϕ ↑P

source

def sylow.subtype {p : ℕ} {G : Type u_1} [group G] (P : sylow p G) {N : subgroup G} (h : ↑P ≤ N) :

sylow p ↥N

A sylow subgroup of G is also a sylow subgroup of a subgroup of G.

Equations

P.subtype h = P.comap_of_injective N.subtype sylow.subtype._proof_1 _

source

@[simp]

theorem sylow.coe_subtype {p : ℕ} {G : Type u_1} [group G] (P : sylow p G) {N : subgroup G} (h : ↑P ≤ N) :

↑(P.subtype h) = subgroup.comap N.subtype ↑P

source

theorem is_p_group.exists_le_sylow {p : ℕ} {G : Type u_1} [group G] {P : subgroup G} (hP : is_p_group p ↥P) :

∃ (Q : sylow p G), P ≤ ↑Q

A generalization of Sylow's first theorem. Every p-subgroup is contained in a Sylow p-subgroup.

source

@[protected, instance]

def sylow.nonempty {p : ℕ} {G : Type u_1} [group G] :

nonempty (sylow p G)

source

@[protected, instance]

noncomputable def sylow.inhabited {p : ℕ} {G : Type u_1} [group G] :

inhabited (sylow p G)

Equations

sylow.inhabited = classical.inhabited_of_nonempty sylow.nonempty

source

theorem sylow.exists_comap_eq_of_ker_is_p_group {p : ℕ} {G : Type u_1} [group G] {H : Type u_2} [group H] (P : sylow p H) {f : H →* G} (hf : is_p_group p ↥(f.ker)) :

∃ (Q : sylow p G), subgroup.comap f ↑Q = ↑P

source

theorem sylow.exists_comap_eq_of_injective {p : ℕ} {G : Type u_1} [group G] {H : Type u_2} [group H] (P : sylow p H) {f : H →* G} (hf : function.injective ⇑f) :

∃ (Q : sylow p G), subgroup.comap f ↑Q = ↑P

source

theorem sylow.exists_comap_subtype_eq {p : ℕ} {G : Type u_1} [group G] {H : subgroup G} (P : sylow p ↥H) :

∃ (Q : sylow p G), subgroup.comap H.subtype ↑Q = ↑P

source

noncomputable def sylow.fintype_of_ker_is_p_group {p : ℕ} {G : Type u_1} [group G] {H : Type u_2} [group H] {f : H →* G} (hf : is_p_group p ↥(f.ker)) [fintype (sylow p G)] :

fintype (sylow p H)

If the kernel of f : H →* G is a p-group, then fintype (sylow p G) implies fintype (sylow p H).

Equations

sylow.fintype_of_ker_is_p_group hf = let h_exists : ∀ (P : sylow p H), ∃ (Q : sylow p G), subgroup.comap f ↑Q = ↑P := _, g : sylow p H → sylow p G := λ (P : sylow p H), classical.some _, hg : ∀ (P : sylow p H), subgroup.comap f (g P).to_subgroup = ↑P := _ in fintype.of_injective g _

source

noncomputable def sylow.fintype_of_injective {p : ℕ} {G : Type u_1} [group G] {H : Type u_2} [group H] {f : H →* G} (hf : function.injective ⇑f) [fintype (sylow p G)] :

fintype (sylow p H)

If f : H →* G is injective, then fintype (sylow p G) implies fintype (sylow p H).

Equations

sylow.fintype_of_injective hf = sylow.fintype_of_ker_is_p_group _

source

@[protected, instance]

noncomputable def sylow.fintype {p : ℕ} {G : Type u_1} [group G] (H : subgroup G) [fintype (sylow p G)] :

fintype (sylow p ↥H)

If H is a subgroup of G, then fintype (sylow p G) implies fintype (sylow p H).

Equations

sylow.fintype H = sylow.fintype_of_injective _

source

@[protected, instance]

def sylow.finite {p : ℕ} {G : Type u_1} [group G] (H : subgroup G) [finite (sylow p G)] :

finite (sylow p ↥H)

If H is a subgroup of G, then finite (sylow p G) implies finite (sylow p H).

source

@[protected, instance]

def sylow.pointwise_mul_action {p : ℕ} {G : Type u_1} [group G] {α : Type u_2} [group α] [mul_distrib_mul_action α G] :

mul_action α (sylow p G)

subgroup.pointwise_mul_action preserves Sylow subgroups.

Equations

sylow.pointwise_mul_action = {to_has_smul := {smul := λ (g : α) (P : sylow p G), {to_subgroup := g • ↑P, is_p_group' := _, is_maximal' := _}}, one_smul := _, mul_smul := _}

source

theorem sylow.pointwise_smul_def {p : ℕ} {G : Type u_1} [group G] {α : Type u_2} [group α] [mul_distrib_mul_action α G] {g : α} {P : sylow p G} :

↑(g • P) = g • ↑P

source

@[protected, instance]

def sylow.mul_action {p : ℕ} {G : Type u_1} [group G] :

mul_action G (sylow p G)

Equations

sylow.mul_action = mul_action.comp_hom (sylow p G) mul_aut.conj

source

theorem sylow.smul_def {p : ℕ} {G : Type u_1} [group G] {g : G} {P : sylow p G} :

g • P = ⇑mul_aut.conj g • P

source

theorem sylow.coe_subgroup_smul {p : ℕ} {G : Type u_1} [group G] {g : G} {P : sylow p G} :

↑(g • P) = ⇑mul_aut.conj g • ↑P

source

theorem sylow.coe_smul {p : ℕ} {G : Type u_1} [group G] {g : G} {P : sylow p G} :

↑(g • P) = ⇑mul_aut.conj g • ↑P

source

theorem sylow.smul_le {p : ℕ} {G : Type u_1} [group G] {P : sylow p G} {H : subgroup G} (hP : ↑P ≤ H) (h : ↥H) :

↑(h • P) ≤ H

source

theorem sylow.smul_subtype {p : ℕ} {G : Type u_1} [group G] {P : sylow p G} {H : subgroup G} (hP : ↑P ≤ H) (h : ↥H) :

h • P.subtype hP = (h • P).subtype _

source

theorem sylow.smul_eq_iff_mem_normalizer {p : ℕ} {G : Type u_1} [group G] {g : G} {P : sylow p G} :

g • P = P ↔ g ∈ ↑P.normalizer

source

theorem sylow.smul_eq_of_normal {p : ℕ} {G : Type u_1} [group G] {g : G} {P : sylow p G} [h : ↑P.normal] :

g • P = P

source

theorem subgroup.sylow_mem_fixed_points_iff {p : ℕ} {G : Type u_1} [group G] (H : subgroup G) {P : sylow p G} :

P ∈ mul_action.fixed_points ↥H (sylow p G) ↔ H ≤ ↑P.normalizer

source

theorem is_p_group.inf_normalizer_sylow {p : ℕ} {G : Type u_1} [group G] {P : subgroup G} (hP : is_p_group p ↥P) (Q : sylow p G) :

P ⊓ ↑Q.normalizer = P ⊓ ↑Q

source

theorem is_p_group.sylow_mem_fixed_points_iff {p : ℕ} {G : Type u_1} [group G] {P : subgroup G} (hP : is_p_group p ↥P) {Q : sylow p G} :

Q ∈ mul_action.fixed_points ↥P (sylow p G) ↔ P ≤ ↑Q

source

@[protected, instance]

def sylow.mul_action.is_pretransitive {p : ℕ} {G : Type u_1} [group G] [hp : fact (nat.prime p)] [finite (sylow p G)] :

mul_action.is_pretransitive G (sylow p G)

A generalization of Sylow's second theorem. If the number of Sylow p-subgroups is finite, then all Sylow p-subgroups are conjugate.

source

theorem card_sylow_modeq_one (p : ℕ) (G : Type u_1) [group G] [fact (nat.prime p)] [fintype (sylow p G)] :

fintype.card (sylow p G) ≡ 1 [MOD p]

A generalization of Sylow's third theorem. If the number of Sylow p-subgroups is finite, then it is congruent to 1 modulo p.

source

theorem not_dvd_card_sylow (p : ℕ) (G : Type u_1) [group G] [hp : fact (nat.prime p)] [fintype (sylow p G)] :

¬p ∣ fintype.card (sylow p G)

source

def sylow.equiv_smul {p : ℕ} {G : Type u_1} [group G] (P : sylow p G) (g : G) :

↥P ≃* ↥(g • P)

Sylow subgroups are isomorphic

Equations

P.equiv_smul g = subgroup.equiv_smul (⇑mul_aut.conj g) ↑P

source

noncomputable def sylow.equiv {p : ℕ} {G : Type u_1} [group G] [fact (nat.prime p)] [finite (sylow p G)] (P Q : sylow p G) :

↥P ≃* ↥Q

Sylow subgroups are isomorphic

Equations

P.equiv Q = _.mpr (P.equiv_smul (classical.some _))

source

@[simp]

theorem sylow.orbit_eq_top {p : ℕ} {G : Type u_1} [group G] [fact (nat.prime p)] [finite (sylow p G)] (P : sylow p G) :

mul_action.orbit G P = ⊤

source

theorem sylow.stabilizer_eq_normalizer {p : ℕ} {G : Type u_1} [group G] (P : sylow p G) :

mul_action.stabilizer G P = ↑P.normalizer

source

noncomputable def sylow.equiv_quotient_normalizer {p : ℕ} {G : Type u_1} [group G] [fact (nat.prime p)] [fintype (sylow p G)] (P : sylow p G) :

sylow p G ≃ G ⧸ ↑P.normalizer

Sylow p-subgroups are in bijection with cosets of the normalizer of a Sylow p-subgroup

Equations

P.equiv_quotient_normalizer = (((equiv.set.univ (sylow p G)).symm.trans (_.mpr (equiv.refl ↥⊤))).trans (mul_action.orbit_equiv_quotient_stabilizer G P)).trans (_.mpr (equiv.refl (G ⧸ ↑P.normalizer)))

source

@[protected, instance]

noncomputable def has_quotient.quotient.fintype {p : ℕ} {G : Type u_1} [group G] [fact (nat.prime p)] [fintype (sylow p G)] (P : sylow p G) :

fintype (G ⧸ ↑P.normalizer)

Equations

has_quotient.quotient.fintype P = fintype.of_equiv (sylow p G) P.equiv_quotient_normalizer

source

theorem card_sylow_eq_card_quotient_normalizer {p : ℕ} {G : Type u_1} [group G] [fact (nat.prime p)] [fintype (sylow p G)] (P : sylow p G) :

fintype.card (sylow p G) = fintype.card (G ⧸ ↑P.normalizer)

source

theorem card_sylow_eq_index_normalizer {p : ℕ} {G : Type u_1} [group G] [fact (nat.prime p)] [fintype (sylow p G)] (P : sylow p G) :

fintype.card (sylow p G) = ↑P.normalizer.index

source

theorem card_sylow_dvd_index {p : ℕ} {G : Type u_1} [group G] [fact (nat.prime p)] [fintype (sylow p G)] (P : sylow p G) :

fintype.card (sylow p G) ∣ ↑P.index

source

theorem not_dvd_index_sylow' {p : ℕ} {G : Type u_1} [group G] [hp : fact (nat.prime p)] (P : sylow p G) [↑P.normal] (hP : ↑P.index ≠ 0) :

¬p ∣ ↑P.index

source

theorem not_dvd_index_sylow {p : ℕ} {G : Type u_1} [group G] [hp : fact (nat.prime p)] [finite (sylow p G)] (P : sylow p G) (hP : ↑P.relindex ↑P.normalizer ≠ 0) :

¬p ∣ ↑P.index

source

theorem sylow.normalizer_sup_eq_top {G : Type u_1} [group G] {p : ℕ} [fact (nat.prime p)] {N : subgroup G} [N.normal] [finite (sylow p ↥N)] (P : sylow p ↥N) :

(subgroup.map N.subtype ↑P).normalizer ⊔ N = ⊤

Frattini's Argument: If N is a normal subgroup of G, and if P is a Sylow p-subgroup of N, then N_G(P) ⊔ N = G.

source

theorem quotient_group.card_preimage_mk {G : Type u} [group G] [fintype G] (s : subgroup G) (t : set (G ⧸ s)) :

fintype.card ↥(quotient_group.mk ⁻¹' t) = fintype.card ↥s * fintype.card ↥t

source

theorem sylow.mem_fixed_points_mul_left_cosets_iff_mem_normalizer {G : Type u} [group G] {H : subgroup G} [finite ↥↑H] {x : G} :

↑x ∈ mul_action.fixed_points ↥H (G ⧸ H) ↔ x ∈ H.normalizer

source

def sylow.fixed_points_mul_left_cosets_equiv_quotient {G : Type u} [group G] (H : subgroup G) [finite ↥↑H] :

↥(mul_action.fixed_points ↥H (G ⧸ H)) ≃ ↥(H.normalizer) ⧸ subgroup.comap H.normalizer.subtype H

The fixed points of the action of H on its cosets correspond to normalizer H / H.

Equations

sylow.fixed_points_mul_left_cosets_equiv_quotient H = equiv.subtype_quotient_equiv_quotient_subtype ↑(H.normalizer) (mul_action.fixed_points ↥H (quotient (id (mul_action.orbit_rel ↥(H.opposite) G)))) _ _

source

theorem sylow.card_quotient_normalizer_modeq_card_quotient {G : Type u} [group G] [fintype G] {p n : ℕ} [hp : fact (nat.prime p)] {H : subgroup G} (hH : fintype.card ↥H = p ^ n) :

fintype.card (↥(H.normalizer) ⧸ subgroup.comap H.normalizer.subtype H) ≡ fintype.card (G ⧸ H) [MOD p]

If H is a p-subgroup of G, then the index of H inside its normalizer is congruent mod p to the index of H.

source

theorem sylow.card_normalizer_modeq_card {G : Type u} [group G] [fintype G] {p n : ℕ} [hp : fact (nat.prime p)] {H : subgroup G} (hH : fintype.card ↥H = p ^ n) :

fintype.card ↥(H.normalizer) ≡ fintype.card G [MOD p ^ (n + 1)]

If H is a subgroup of G of cardinality p ^ n, then the cardinality of the normalizer of H is congruent mod p ^ (n + 1) to the cardinality of G.

source

theorem sylow.prime_dvd_card_quotient_normalizer {G : Type u} [group G] [fintype G] {p n : ℕ} [hp : fact (nat.prime p)] (hdvd : p ^ (n + 1) ∣ fintype.card G) {H : subgroup G} (hH : fintype.card ↥H = p ^ n) :

p ∣ fintype.card (↥(H.normalizer) ⧸ subgroup.comap H.normalizer.subtype H)

If H is a p-subgroup but not a Sylow p-subgroup, then p divides the index of H inside its normalizer.

source

theorem sylow.prime_pow_dvd_card_normalizer {G : Type u} [group G] [fintype G] {p n : ℕ} [hp : fact (nat.prime p)] (hdvd : p ^ (n + 1) ∣ fintype.card G) {H : subgroup G} (hH : fintype.card ↥H = p ^ n) :

p ^ (n + 1) ∣ fintype.card ↥(H.normalizer)

If H is a p-subgroup but not a Sylow p-subgroup of cardinality p ^ n, then p ^ (n + 1) divides the cardinality of the normalizer of H.

source

theorem sylow.exists_subgroup_card_pow_succ {G : Type u} [group G] [fintype G] {p n : ℕ} [hp : fact (nat.prime p)] (hdvd : p ^ (n + 1) ∣ fintype.card G) {H : subgroup G} (hH : fintype.card ↥H = p ^ n) :

∃ (K : subgroup G), fintype.card ↥K = p ^ (n + 1) ∧ H ≤ K

If H is a subgroup of G of cardinality p ^ n, then H is contained in a subgroup of cardinality p ^ (n + 1) if p ^ (n + 1) divides the cardinality of G

source

theorem sylow.exists_subgroup_card_pow_prime_le {G : Type u} [group G] [fintype G] (p : ℕ) {n m : ℕ} [hp : fact (nat.prime p)] (hdvd : p ^ m ∣ fintype.card G) (H : subgroup G) (hH : fintype.card ↥H = p ^ n) (hnm : n ≤ m) :

∃ (K : subgroup G), fintype.card ↥K = p ^ m ∧ H ≤ K

If H is a subgroup of G of cardinality p ^ n, then H is contained in a subgroup of cardinality p ^ m if n ≤ m and p ^ m divides the cardinality of G

source

theorem sylow.exists_subgroup_card_pow_prime {G : Type u} [group G] [fintype G] (p : ℕ) {n : ℕ} [fact (nat.prime p)] (hdvd : p ^ n ∣ fintype.card G) :

∃ (K : subgroup G), fintype.card ↥K = p ^ n

A generalisation of Sylow's first theorem. If p ^ n divides the cardinality of G, then there is a subgroup of cardinality p ^ n

source

theorem sylow.pow_dvd_card_of_pow_dvd_card {G : Type u} [group G] [fintype G] {p n : ℕ} [hp : fact (nat.prime p)] (P : sylow p G) (hdvd : p ^ n ∣ fintype.card G) :

p ^ n ∣ fintype.card ↥P

source

theorem sylow.dvd_card_of_dvd_card {G : Type u} [group G] [fintype G] {p : ℕ} [fact (nat.prime p)] (P : sylow p G) (hdvd : p ∣ fintype.card G) :

p ∣ fintype.card ↥P

source

theorem sylow.card_coprime_index {G : Type u} [group G] [fintype G] {p : ℕ} [hp : fact (nat.prime p)] (P : sylow p G) :

(fintype.card ↥P).coprime ↑P.index

Sylow subgroups are Hall subgroups.

source

theorem sylow.ne_bot_of_dvd_card {G : Type u} [group G] [fintype G] {p : ℕ} [hp : fact (nat.prime p)] (P : sylow p G) (hdvd : p ∣ fintype.card G) :

↑P ≠ ⊥

source

theorem sylow.card_eq_multiplicity {G : Type u} [group G] [fintype G] {p : ℕ} [hp : fact (nat.prime p)] (P : sylow p G) :

fintype.card ↥P = p ^ ⇑((fintype.card G).factorization) p

The cardinality of a Sylow group is p ^ n where n is the multiplicity of p in the group order.

source

theorem sylow.subsingleton_of_normal {G : Type u} [group G] {p : ℕ} [fact (nat.prime p)] [finite (sylow p G)] (P : sylow p G) (h : ↑P.normal) :

subsingleton (sylow p G)

source

theorem sylow.characteristic_of_normal {G : Type u} [group G] {p : ℕ} [fact (nat.prime p)] [finite (sylow p G)] (P : sylow p G) (h : ↑P.normal) :

↑P.characteristic

source

theorem sylow.normal_of_normalizer_normal {G : Type u} [group G] {p : ℕ} [fact (nat.prime p)] [finite (sylow p G)] (P : sylow p G) (hn : ↑P.normalizer.normal) :

↑P.normal

source

@[simp]

theorem sylow.normalizer_normalizer {G : Type u} [group G] {p : ℕ} [fact (nat.prime p)] [finite (sylow p G)] (P : sylow p G) :

↑P.normalizer.normalizer = ↑P.normalizer

source

theorem sylow.normal_of_all_max_subgroups_normal {G : Type u} [group G] [finite G] (hnc : ∀ (H : subgroup G), is_coatom H → H.normal) {p : ℕ} [fact (nat.prime p)] [finite (sylow p G)] (P : sylow p G) :

↑P.normal

source

theorem sylow.normal_of_normalizer_condition {G : Type u} [group G] (hnc : normalizer_condition G) {p : ℕ} [fact (nat.prime p)] [finite (sylow p G)] (P : sylow p G) :

↑P.normal

source

noncomputable def sylow.direct_product_of_normal {G : Type u} [group G] [fintype G] (hn : ∀ {p : ℕ} [_inst_3 : fact (nat.prime p)] (P : sylow p G), ↑P.normal) :

(Π (p : ↥((fintype.card G).factorization.support)) (P : sylow ↑p G), ↥↑P) ≃* G

If all its sylow groups are normal, then a finite group is isomorphic to the direct product of these sylow groups.

Equations

sylow.direct_product_of_normal hn = let ps : finset ℕ := (fintype.card G).factorization.support in id (let P : Π (p : ℕ), sylow p G := inhabited.default in (id (mul_equiv.Pi_congr_right (λ (j : ↥ps), subtype.cases_on j (λ (p : ℕ) (hp : p ∈ ps), id (mul_equiv.Pi_subsingleton (λ (P : sylow p G), ↥P) (P p)))))).trans (id (mul_equiv.of_bijective (subgroup.noncomm_pi_coprod _) _)))