Finite field extensions

Stream: Is there code for X?

[Wrenna Robson]

What's the right way to talk about finite field extensions of zmod p (p prime), where I might want to do things like assert that field members of the extension are in the subfield?

[Kevin Buzzard]

I would go for a type k which is a field, an algebra for zmod p and which is finite-dimensional. If you want the subfield of k corresponding to this you'll probably have to make it explicitly..

[Johan Commelin]

There's quite a library about intermediate fields. And in particular the \top intermediate field.

[Wrenna Robson]

Do we have that it follows that the char of k is p?

[Eric Wieser]

I think docs#algebra.char_p_iff will work there?

[Eric Wieser]

There won't be an instance

[Wrenna Robson]

Perfect - thanks.