Z-Groups

A Z-group is a group whose Sylow subgroups are all cyclic.

Main definitions

• IsZGroup G: A predicate stating that all Sylow subgroups of G are cyclic.

TODO: Show that if G is a Z-group with commutator subgroup G', then G = G' ⋊ G/G' where G' and G/G' are cyclic of coprime orders.

class IsZGroup (G : Type u_1) [Group G] : Prop

A Z-group is a group whose Sylow subgroups are all cyclic.

• isZGroup : ∀ (p : ℕ), Nat.Prime p → ∀ (P : Sylow p G), IsCyclic ↥↑P

theorem isZGroup_iff (G : Type u_1) [Group G] : IsZGroup G ↔ ∀ (p : ℕ), Nat.Prime p → ∀ (P : Sylow p G), IsCyclic ↥↑P

theorem IsZGroup.of_squarefree {G : Type u_1} [Group G] (hG : Squarefree (Nat.card G)) : IsZGroup G

theorem IsZGroup.of_injective {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] {f : G →* G'} [hG' : IsZGroup G'] (hf : Function.Injective ⇑f) : IsZGroup G

instance IsZGroup.instSubtypeMemSubgroup {G : Type u_1} [Group G] [IsZGroup G] (H : Subgroup G) : IsZGroup ↥H

Equations

• ⋯ = ⋯

theorem IsZGroup.of_surjective {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] {f : G →* G'} [Finite G] [hG : IsZGroup G] (hf : Function.Surjective ⇑f) : IsZGroup G'

instance IsZGroup.instQuotientSubgroupOfFinite {G : Type u_1} [Group G] [Finite G] [IsZGroup G] (H : Subgroup G) [H.Normal] : IsZGroup (G ⧸ H)

Equations

• ⋯ = ⋯