Galois theory of finite fields

Stream: mathlib4

[Johan Commelin]

How far are the main statements of Galois theory for finite fields from mathlib?

• every extension of finite fields is Galois
• the Galois group is cyclic
• generated by Frobenius

[Andrew Yang]

I assume you mean finite extension (or at least algebraic)?
I think the folder FieldTheory/Finite/* is all we have in mathlib. We don't even know what $\overline{\mathbb{F}_q}$ is.

[Johan Commelin]

I meant L/K where both L and K are finite fields, so the extension will certainly be finite and algebraic.

[Adam Topaz]

I think we have all the ingredients to make these proofs relatively easy

[Junyan Xu]

Some work at https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Algebraic.20Conjugate.20over.20Finite.20Fields/near/402812924 in Lean 3 that is not yet PR'd.

[Andrew Yang]

We have docs#GaloisField.instIsGalois