[Merged by Bors] - feat(field_theory): prove primitive element theorem

[tb65536]

Proof of the primitive element theorem. The main proof is in field_theory/primitive_element.lean. Some lemmas we used have been added to other files. We have also changed the notation for adjoining an element to a field to be easier to use.

[jcommelin]

This is starting to look really good.

[jcommelin]

This is your main result, and this is what you want others to use. Please consider writing a more detailed docstring. Out of context "complete" doesn't make sense. It's only the rush of victory when you read through this file that explains it 😜
It's good to just quote the informal theorem in the docstring, since this is an important result.

Also, I know that it feels like an abomination, but consider renaming this to exists_adjoin_simple_eq_top or something like that. Because primitive elements haven't been formally defined in Lean.
Certainly the docstring should mention "primitive element theorem" so that people can find this result!

[pglutz]

How about this for the docstring:

Primitive element theorem: a finite separable field extension `E` of `F` has a
primitive element, i.e. there is an `α ∈ E` such that `F⟮α⟯ = (⊤ : subalgebra F E)`.

[pglutz]

Okay, I changed the name of primitive_element 😢 Should we also change the names of the lemmas in that file (which right now are called primitive_element_two_inf and so on)?

[Vierkantor]

Although consistency is good, I'm not so convinced that exists_adjoin_simple_eq_top_two_inf is the most readable or useful name. If you're up for some bikeshedding: how about defining something like @[reducible] def is_primitive_element (K : Type*) [field K] {L : Type*} [field K] [algebra K L] (x : L) := field.adjoin K {x} = ⊤ at the top of the file, and prefix exists_ in front of primitive_element in this file? So we get names like exists_primitive_element_two_inf.

[pglutz]

I also don't really like exists_adjoin_simple_eq_top and it could be confusing to have lemmas in the file with primitive_element in their title when the main result doesn't (and on the other hand, renaming those lemmas could result in some really ugly names). Also, we tried using your suggested definition of is_primitive_element and it worked but made proofs a little longer (a lot of times it was necessary to add an extra line to unfold is_primitive_element because it was confusing the rewrite tactic) without much obvious benefit (to me at least). So here's my proposal: we name everything exists_primitive_element (and similarly exists_primitive_element_inf and so on) but otherwise keep the names, etc, as is. If that doesn't seem like a reasonable idea, let us know and we can definitely change it.

[pglutz]

Also, Thomas has pointed out that exists_adjoin_simple_eq_top leaves out the important hypothesis that the field extension is separable, but anything that has primitive_element in the name makes that clear.

[Vierkantor]

I think exists_primitive_element is a good compromise, if we put an implementation note in the module documentation. (I put a suggestion there.)

[Vierkantor]

Thanks for all the changes! I'm happy with how the PR is looking now, just some tiny remarks. I don't care too much about names as long as they are guessable, but in the spirit of bikeshedding, these are my favourite options.

[jcommelin]

This is great. Thanks a lot. And I'm happy with the names. 👍
I'll let @Vierkantor do the honours of kicking this on the merge queue.

[Vierkantor]

Let's do this!

bors r+

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Run tests