Zulip Chat Archive

Stream: Is there code for X?

Topic: Every finite division ring is a field

Jiang Jiedong (Dec 08 2023 at 15:18):

Hi everyone,
Is the theorem of "every finite division ring is a field" already formalized in mathlib? If yes, what is it called? Thank you!

Floris van Doorn (Dec 08 2023 at 15:20):

docs#Fintype.fieldOfDomain Every finite commutative domain is a field.

Jiang Jiedong (Dec 08 2023 at 15:22):

Floris van Doorn said:

docs#Fintype.fieldOfDomain Every finite commutative domain is a field.

Thanks!
What about non-commutative case?

Floris van Doorn (Dec 08 2023 at 15:22):

oh wait, I missed the commutative condition. According to the docstring that is still a todo.

Floris van Doorn (Dec 08 2023 at 15:23):

so it's not yet in mathlib.

Riccardo Brasca (Dec 08 2023 at 15:23):

@Eric Rodriguez knows

Riccardo Brasca (Dec 08 2023 at 15:23):

There is a PR

Riccardo Brasca (Dec 08 2023 at 15:23):

(deleted)

Riccardo Brasca (Dec 08 2023 at 15:24):

(deleted)

Floris van Doorn (Dec 08 2023 at 15:24):

#6800

Riccardo Brasca (Dec 08 2023 at 15:25):

Anyway it is almost ready, I think only the docstring needs a little improvement

Notification Bot (Dec 08 2023 at 15:26):

Jiang Jiedong has marked this topic as resolved.

Eric Rodriguez (Dec 08 2023 at 15:30):

Yeah I was waiting for the simp zeta changes but I think I'll just give in and do it by hand and turn off zeta in every simp in that proof and slam a big todo

Eric Rodriguez (Dec 12 2023 at 18:06):

I've significantly tidied the proof and pished a new version:)

Notification Bot (Dec 12 2023 at 19:06):

Oliver Nash has marked this topic as unresolved.

Oliver Nash (Dec 12 2023 at 19:09):

Ages ago I came across this https://arxiv.org/abs/1805.11451 and thought it might be fun to formalise (assuming it is correct).

Riccardo Brasca (Dec 12 2023 at 19:16):

If I remember correctly it is also true that a division ring such that every element is of finite order is commutative

Patrick Massot (Dec 12 2023 at 19:20):

Yes, this is a corollary of what Oliver refers to.

Riccardo Brasca (Dec 13 2023 at 10:41):

I mean without assuming finiteness: a ring R such that for all x : R there is n (depending on x) such that x ^ n = x is commutative.

Eric Rodriguez (Dec 13 2023 at 10:42):

Yes, it's not proved in this paper but it's mentioned as a folklore result of Jacobson

Eric Rodriguez (Dec 13 2023 at 10:50):

https://www.cambridge.org/core/services/aop-cambridge-core/content/view/1357951822F180A979D1D3719CF8DECE/S0008439500062123a.pdf/a-proof-of-jacobsons-theorem.pdf

doesn't seem too awful either

Riccardo Brasca (Dec 13 2023 at 11:59):

#6800 is (almost) ready to go

Last updated: Dec 20 2023 at 11:08 UTC