Wedderburn's little theorem

Stream: Is there code for X?

[Anatole Dedecker]

Does Lean know that any finite division ring is a field ?

[Ruben Van de Velde]

I think yes for division rings, but not for domains, but I can't find it now

[Ruben Van de Velde]

https://leanprover-community.github.io/mathlib_docs/ring_theory/integral_domain.html#field_of_integral_domain

[Anatole Dedecker]

But you still need commutativity to get integral_domain right ? I was thinking about the fact that finiteness and inversibility for nonzero elements imply commutativity

[Johan Commelin]

But that's a bit more work than integral_domain → field. It's definitely something we want in mathlib! First computation of a Brauer group in mathlib (-;

[Anatole Dedecker]

If it's not there that's something I may like to work on :)

[Kevin Buzzard]

yes, the division ring statement is far harder than the integral domain statement, which is just counting.

[Johan Commelin]

All the ingredients are there: https://en.wikipedia.org/wiki/Wedderburn%27s_little_theorem#Proof

[Johan Commelin]

I think this would be a very nice test of combining several parts of mathlib.

[Johan Commelin]

@Anatole Dedecker This sounds like a really nice project. Please keep me posted about how it goes!

[Johan Commelin]

Btw, here's a formalization in Mizar: http://mizar.org/version/current/html/weddwitt.html

[Johan Commelin]

Although I think that the proof that is in Wiki should be more or less directly transferable to Lean

[Kevin Buzzard]

If I understand correctly that Mizar link is missing all the proofs (but the statements are pleasingly readable, modulo lack of unicode)

[Johan Commelin]

@Kevin Buzzard If you click on proof it will expand

[Kevin Buzzard]

...to something which doesn't fit on my screen and can't be scrolled :-/ aah, I see, click, don't hover.

[Johan Commelin]

you shouldn't try to read proofs on your phone while still in bed (-;
that's why they presented you with just the statements to begin with :rofl:

[Johan Commelin]

@Anatole Dedecker Oops, I forgot about this. I formalised a proof now https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/.239856.20little.20wedderburn.
Did you already start working on this? If so, I'm sorry for scooping. My apologies.

[Anatole Dedecker]

No worries. I did start working on it but I didn't do much (I've been pretty bad at managing my todo-list recently), so that's really not a problem.