## Stream: maths

### Topic: squeeze_ring

#### Kevin Buzzard (Apr 08 2020 at 18:27):

So I am very pleased to see that nobody other than @Kenny Lau can do the codewars Kata about proving that no commutative ring has 5 units. I wrote a proof which compiles fine but takes around 10 seconds on my machine, which is too long for the codewars servers. In short, I have to optimise my code. One way of perhaps saving some time would be to replace all occurrences of ring or ring_exp with an explicit list of rewrites :-) I have absolutely no idea how close to being possible that is :-)

#### Alex J. Best (Apr 08 2020 at 18:28):

Hey, I can do it!! My proof is just over 16000 ms :frown: :anguish:

#### Kevin Buzzard (Apr 08 2020 at 18:29):

Yeah, you can "do" it like I can do it, i.e. it times out :-)

Try submitting it 100 times and see if you get lucky? :-)

#### Kevin Buzzard (Apr 08 2020 at 18:30):

Gratz on the maths proof, by the way! It's tricky to formalise in Lean!

#### Alex J. Best (Apr 08 2020 at 18:30):

Yes I've tried! but no luck so far, maybe I should find a time of the night the codewars servers are least loaded?

#### Alex J. Best (Apr 08 2020 at 18:31):

Yeah it was a fun problem so thanks to you both for putting it up! And for everyone who got codewars running in the first place!

#### orlando (Apr 08 2020 at 19:09):

@Kevin Buzzard You show that if $G$ is a group and $\text{Card}(G) \leq 4$ then $G$ is commutative ?

#### Kevin Buzzard (Apr 08 2020 at 19:12):

The lemma is that no $R$ has $|R^\times|=5$

#### Kevin Buzzard (Apr 08 2020 at 19:13):

although that looks like another fabulous kata :-)

#### Kenny Lau (Apr 08 2020 at 19:14):

it follows from p is commutative and p^2 is commutative

#### Kevin Buzzard (Apr 08 2020 at 19:14):

Do we have that in Lean?

#### Kevin Buzzard (Apr 08 2020 at 19:14):

and anyway, you missed out the case $p^0$

#### Kenny Lau (Apr 08 2020 at 19:14):

the case for 1 is a bunch of subsingleton elim

#### Kenny Lau (Apr 08 2020 at 19:14):

maybe we can have a kata proving p^2 is commutative

#### Kenny Lau (Apr 08 2020 at 19:15):

and if we go on we'll recreate @Chris Hughes' Sylow's theorems

#### Kevin Buzzard (Apr 08 2020 at 19:15):

aah, any group of order $p^0$ embeds in a group of size $p^1$ so it follows from the $p^1$ case.