feat(field_theory/splitting_field): Adjoining all of the roots of a polynomial gives a splitting field

[tb65536]

This PR proves that if p splits in a field extensions, then adjoining all of the roots of p gives a splitting field of p.

---

• [x] depends on: #15658
• [x] depends on: #15743
• [x] depends on: #15745
• [x] depends on: #15762

[mathlib-dependent-issues-bot]

This PR/issue depends on:

• ~~leanprover-community/mathlib#15658~~
• ~~leanprover-community/mathlib#15743~~
• ~~leanprover-community/mathlib#15745~~
• ~~leanprover-community/mathlib#15762~~ By Dependent Issues (🤖). Happy coding!

[bors[bot]]

Build failed (retrying...):

• Build mathlib

[bors[bot]]

Build failed (retrying...):

• Build mathlib

[bors[bot]]

Build failed (retrying...):

• Build mathlib
• Lint mathlib
• Run tests

[jcommelin]

bors merge p=4

[bors[bot]]

Build failed (retrying...):

• Build mathlib

[bors[bot]]

Pull request successfully merged into master.

Build succeeded:

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