Discussions "Groups of order pq"

Stream: general

[Peiran Wu]

Announcement: https://leanprover.zulipchat.com/#narrow/channel/113486-announce/topic/Groups.20of.20order.20pq/near/479713435

Source code: https://github.com/wupr/order-p-q

[Thomas Browning]

More generally, it would be worth proving that if all Sylow subgroups of a finite group $G$ are cyclic, then $G\cong G'\rtimes G/G'$, where $G'$ and $G/G'$ are cyclic with coprime order. This is Theorem 5.16 of Isaac's Finite Group Theory.

[Thomas Browning]

It seems like the main ingredients are Burnside's normal p-complement theorem and the Schur-Zassenhaus theorem, which we already have in mathlib.

[Junyan Xu]

Hmmm, this is the same Isaacs as in #18412.

[Thomas Browning]

Just noting that a classification of groups of squarefree order is close now: #20358