Extensions of finite fields are Galois?

Stream: Is there code for X?

[Michael Stoll]

I can't find the statement that extensions of finite fields are Galois in mathlib. I would think it should be there, though.

[Thomas Browning]

Can't find it either on a first glance, but it should be easy from the following:
docs#is_galois.of_separable_splitting_field
docs#galois_poly_separable
docs#galois_field.has_sub.sub.polynomial.is_splitting_field or docs#galois_field.is_splitting_field_of_card_eq

[Michael Stoll]

I don't claim it's difficult; my claim is that it should be there. I'll try to put a proof together tomorrow and set up a PR.

[Thomas Browning]

#14290
I hope you don't mind me beating you to it :)

[Michael Stoll]

Not at all!
I've left a comment asking for a more general instance, though.

[Mauricio Collares]

Perhaps you started a review but didn't finish it yet? Comments from an in-progress review don't show up to other people, and I can't see yours in the above PR (might be my fault, though).

[Michael Stoll]

Sorry, hit the wrong button. It should be a comment now.