## Stream: maths

### Topic: finite fields

#### Joey van Langen (Jan 09 2019 at 15:09):

I'm going to do some works concerning finite fields. (number of elements, existence and uniqueness)
Can anyone tell me if the following things exist for lean in mathlib or somewhere else and where I can find them?
Integers modulo a prime, prime subfields, ring isomorphisms?

#### Rob Lewis (Jan 09 2019 at 15:14):

Integers mod a prime are at least instantiated as a field: https://github.com/leanprover/mathlib/blob/master/data/zmod/basic.lean#L313

#### Rob Lewis (Jan 09 2019 at 15:16):

Others will probably know more about your other questions. (@Kenny Lau ?)

#### Kenny Lau (Jan 09 2019 at 15:17):

ik ben aan het bezoeken in de stedelijk museum :p

#### Joey van Langen (Jan 09 2019 at 15:17):

Integers modulo p is a nice start

#### Rob Lewis (Jan 09 2019 at 15:18):

I'm glad someone is taking my suggestion to relax this afternoon!

#### Joey van Langen (Jan 09 2019 at 15:18):

Do isomorphisms exist in any context? I can only find them for types

use hott!

#### Joey van Langen (Jan 09 2019 at 15:24):

what do you mean by use hott?

#### Kevin Buzzard (Jan 09 2019 at 15:37):

he's just trolling. He says "use something other than Lean"

#### Kevin Buzzard (Jan 09 2019 at 15:38):

But I guess the answer to your question is that in general most objects don't have isomorphism between those objects already defined in Lean.

#### Kevin Buzzard (Jan 09 2019 at 15:39):

You are more likely to find morphisms though, so you can define isomorphisms without too much pain. I guess morphisms of rings will be there somewhere.

#### Kevin Buzzard (Jan 09 2019 at 15:40):

Some students at Imperial have done some work on splitting fields, but I don't know if it's public. What is your proposal for defining a finite field? Usually the definition I give is "splitting field of $X^{p^n}-X$ over $\mathbb{F}_p$, but I don't think Lean has splitting fields, at least not publically.

#### Joey van Langen (Jan 09 2019 at 15:41):

I'm going to use the definition as a splitting field, by using the splitting field stuff currently in the community repo

#### Joey van Langen (Jan 09 2019 at 15:45):

I will also use the material there concerning algebras as it will give me the tools to realize any finite field as a vector space over $\mathbb{F}_p$

#### Joey van Langen (Jan 09 2019 at 15:45):

How do you put latex in these messages?

#### Kevin Buzzard (Jan 09 2019 at 15:46):

$\mathbb{F}_p$

#### Kevin Buzzard (Jan 09 2019 at 15:46):

Doesn't always work, for example \sqrt doesn't seem to work

#### Joey van Langen (Jan 11 2019 at 15:14):

So I have been doing some work on the finite fields with the help of @Casper Putz for the past couple of days.
We are now close to proving that every finite field has p^n elements with p a prime number.
Most effort was spent proving some simple results which we couldn't find anywhere,
such as the specification of the prime ideals and maximal ideals of $\mathbb{Z}$ and proving that the zero ideal in a field is in fact maximal.
Would people be interested in seeing these results added to mathlib separately? They seem quite useful

Yes

#### Joey van Langen (Jan 11 2019 at 15:32):

Any suggestions of where to put that stuff?

#### Johan Commelin (Jan 11 2019 at 15:33):

Do you guys have push access to https://github.com/leanprover-community/mathlib/ ?

#### Joey van Langen (Jan 11 2019 at 15:33):

For example should the explicit specification of the prime ideals of the integers be put with ideals, with the integers or a separate file entirely

#### Johan Commelin (Jan 11 2019 at 15:33):

If so, put it on a branch finite_fields in that repo.

#### Johan Commelin (Jan 11 2019 at 15:34):

Aaah, I'm always bad at deciding what should go in which file.

#### Joey van Langen (Jan 11 2019 at 15:34):

Do you guys have push access to https://github.com/leanprover-community/mathlib/ ?

We don't have access to the leanprover-community yet. Would be nice to have

#### Joey van Langen (Jan 11 2019 at 15:35):

We're still working on it on my github, but after some cleanup that would probably be the best place to put it

#### Chris Hughes (Jan 11 2019 at 15:35):

It basically depends on imports. Probably ideals imports everything you need, so it should probably go there.

#### Johan Commelin (Jan 11 2019 at 16:00):

@Mario Carneiro Could you please give @Joey van Langen push access on community mathlib? He's a PhD student of Sander Dahmen.

Last updated: May 14 2021 at 19:21 UTC