squeeze_ring

Stream: maths

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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]

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

[Alex J. Best]

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]

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]

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

[orlando]

hum i missread ! :confused:

[Kevin Buzzard]

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

[Kevin Buzzard]

although that looks like another fabulous kata :-)

[Kenny Lau]

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

[Kevin Buzzard]

Do we have that in Lean?

[Kevin Buzzard]

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

[Kenny Lau]

the case for 1 is a bunch of subsingleton elim

[Kenny Lau]

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

[Kenny Lau]

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

[Kevin Buzzard]

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

[Kenny Lau]

sorry you already used subsingleton