a problem with simple groups

Stream: new members

[Billlie Franch]

I would like to ask if someone knows how to formalize this problem: Groups of order pq are not simple, where p and q are prime numbers

[Julian Berman]

Do you perhaps know how to write down parts of that? Perhaps how to write down that G is a group and that it's order is p * q? If so it's good to write down what you know and folks can help fill in the rest

[Notification Bot]

2 messages were moved here from #new members > a problem by Eric Wieser.

[Billlie Franch]

Julian Berman said:

Do you perhaps know how to write down parts of that? Perhaps how to write down that G is a group and that it's order is p * q? If so it's good to write down what you know and folks can help fill in the rest

sorry,I don't know how to describe that its order is p * q，can you help me ?

[Thomas Browning]

You could use something like Nat.card G = p * q

[Billlie Franch]

Can someone tell me how 'p and q are different prime numbers' should be expressed in lean4

[Johan Commelin]

variable (p q : \N) (hp : p.Prime) (hq : q.Prime) (hpq : p \ne q)

[Notification Bot]

Billlie Franch has marked this topic as resolved.

[Billlie Franch]

Johan Commelin said:

variable (p q : \N) (hp : p.Prime) (hq : q.Prime) (hpq : p \ne q)

Thank you very much for your answer, I also want to ask how to express the conclusion that a group is not simple

[Johan Commelin]

Do you know how to express that a group is simple?

[Johan Commelin]

If you go to https://leanprover-community.github.io/, you can click on "API documentation" in the sidebar menu, which will take you to https://leanprover-community.github.io/mathlib4_docs/.

Now start typing simplegroup in the search bar, top right. You should get useful results.

[Notification Bot]

Scott Morrison has marked this topic as unresolved.