a problem in group

Stream: mathlib4

[Steven]

where can i study to solve this problem :G is a group ,p is a prime and p|card(G),then the number of solutions of x^p=1 can be devided by p

[Steven]

this seem to use sylow to prove,which is very easy in math

[Steven]

Let G be a finite group and p be a prime factor of ∣G∣, then p divides the number of solutions to the equation xp=1 in G.it can be solved easily in math by sylow 3 theorem,but i cant solve it in lean,can anyone tell me where can i study the skills in writing this in lean? :cold_sweat:

[Ruben Van de Velde]

Have you managed to write the statement?

[Ruben Van de Velde]

Please don't double post

[ohhaimark]

@Ruben Van de Velde Is this at me. I only posted here AFAIK.

[Ruben Van de Velde]

No, at @Steven

[Notification Bot]

5 messages were moved here from #lean4 > Getting usable constructors from an inductive type. by Kevin Buzzard.

[Kevin Buzzard]

I moved the other messages here, I think it's less confusing (they were in someone else's thread). @Steven your first step is to state the theorem in Lean.

[Steven]

sorry,i dont know how to delete a post,i havent formalize the theorem totally,maybe i will post my progress tomorrow

[Steven]

Ruben Van de Velde said:

Please don't double post

very sorry about that,i dont know how to post before... :confounded: