[Merged by Bors] - feat(field_theory/is_alg_closed/algebraic_closure): add instances normal and is_galois for algebraic closure

[xroblot]

---

[riccardobrasca]

If it's not too much work can you add the is_galois instance (if not already there) in characteristic zero?

[Vierkantor]

Thanks! Looks good to me with Riccardo's suggestion.

bors d+

[bors]

✌️ xroblot can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[xroblot]

Thanks! Looks good to me with Riccardo's suggestion.

bors d+

Ok, thanks. I'll add the is_galois results first.

[xroblot]

I have made significant changes to this PR after it was delegated so I'd like to have another pair of eyes look at it before I hit the merge button.

[riccardobrasca]

Can you just check if infer_instance works where it should? For example in

instance : normal k (algebraic_closure k) := is_alg_closure.normal _ _

[xroblot]

Can you just check if infer_instance works where it should? For example in

instance : normal k (algebraic_closure k) := is_alg_closure.normal _ _

I can confirm the instances are working: I am using them in another PR ;)

[riccardobrasca]

Can you just check if infer_instance works where it should? For example in

instance : normal k (algebraic_closure k) := is_alg_closure.normal _ _

I can confirm the instances are working: I am using them in another PR ;)

I mean as proof of this lemma. If it does than there is no need for it.

In any case this still LGTM.

bors d+

[bors]

✌️ xroblot can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[xroblot]

Can you just check if infer_instance works where it should? For example in

instance : normal k (algebraic_closure k) := is_alg_closure.normal _ _

I can confirm the instances are working: I am using them in another PR ;)

I mean as proof of this lemma. If it does than there is no need for it.

Oh, yes, I see what you mean. Indeed, the proofs of normal, is_separable and is_galois can be generated automatically
by infer_instance for algebraic_closure so I'll remove those instances.

Thanks!

[xroblot]

bors r+

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests