# Zulip Chat Archive

## Stream: Is there code for X?

### Topic: A finite division ring is a field

#### Kevin Buzzard (Jun 05 2020 at 13:26):

Do we have that a finite division ring is a field?

#### Chris Hughes (Jun 05 2020 at 13:27):

Yes

#### Chris Hughes (Jun 05 2020 at 13:27):

No

#### Chris Hughes (Jun 05 2020 at 13:27):

Sorry. We have that a finite integral domain is a field.

#### Kevin Buzzard (Jun 05 2020 at 13:31):

What I'm asking is harder. I guess I know some really stupid proof involving Brauer groups and Galois cohomology but there will be some more basic proof which doesn't need any of that machinery

#### Johan Commelin (Jun 05 2020 at 13:33):

The stupid proof exists. My non-constructive proof of that fact is that I remember seeing a talk about it in a first year student seminar.

#### Johan Commelin (Jun 05 2020 at 13:37):

I didn't read this text: https://www.imsc.res.in/~knr/past/salem1612.pdf but it is probably formalizable

#### Johan Commelin (Jun 05 2020 at 13:38):

Or this one: https://groupprops.subwiki.org/wiki/Every_finite_division_ring_is_a_field

#### David Wärn (Jun 05 2020 at 14:13):

Iirc this is one of the very first results in "Proofs from the Book", after Bertrand's postulate

#### Filippo A. E. Nuccio (Jun 09 2020 at 06:57):

Johan Commelin said:

Or this one: https://groupprops.subwiki.org/wiki/Every_finite_division_ring_is_a_field

This one is indeed quite basic, I studied it in my first year of undergraduate, taken from Herstein "Topics in Algebra": I knew nothing about cohomology (and almost nothing about Galois theory).

#### Johan Commelin (Jun 09 2020 at 07:01):

Do you want to try it?

Last updated: May 07 2021 at 21:10 UTC