The Artin–Wedderburn theorem

The classical Artin–Wedderburn theorem: a nontrivial prime artinian ring is ring-isomorphic to a matrix ring over a division ring. Specialised to a simple ring it yields the same conclusion.

theorem LeanPool.ArtinWedderburn.ArtinWedderburnForPrime {R : Type u} [Ring R] [h_nontriv : Nontrivial R] (h_prime : IsPrimeRing R) (h_artinian : IsArtinian R R) : ∃ (n : ℕ) (D : Type u) (x : DivisionRing D), Nonempty (R ≃+* Matrix (Fin n) (Fin n) D)

theorem LeanPool.ArtinWedderburn.ArtinWedderburnForSimple {R : Type u} [Ring R] [IsSimpleRing R] [h_art : IsArtinian R R] : ∃ (n : ℕ) (D : Type u) (x : DivisionRing D), Nonempty (R ≃+* Matrix (Fin n) (Fin n) D)