feat(ring_theory): Wedderburn's little theorem (finite domains are fields)

[jcommelin]

---

• [x] depends on: #9846
• [x] depends on: #12382
• [x] depends on: #12383
• [x] depends on: #12426
• [x] depends on: #12428
• [x] depends on: #12595
• [x] depends on: #13943
• [x] depends on: #18861
• [x] depends on: #18862

[riccardobrasca]

I think you can extract a PR about the centralizer (including some of the results that are in wedderburn.lean bout rings). And this one is almost ready for review!

[ericrbg]

only slightly less than a year later: #18861! (also #18862 for some misc lemmas). I should be getting this done soon, fingers crossed.

[mathlib-dependent-issues-bot]

This PR/issue depends on:

• ~~leanprover-community/mathlib#9846~~
• ~~leanprover-community/mathlib#12382~~
• ~~leanprover-community/mathlib#12383~~
• ~~leanprover-community/mathlib#12426~~
• ~~leanprover-community/mathlib#12428~~
• ~~leanprover-community/mathlib#12595~~
• ~~leanprover-community/mathlib#13943~~
• ~~leanprover-community/mathlib#18861~~
• ~~leanprover-community/mathlib#18862~~ By Dependent Issues (🤖). Happy coding!