Wedderburn–Artin Theorem over an algebraically closed field

theorem IsSimpleRing.exists_algEquiv_matrix_of_isAlgClosed (F : Type u_1) (R : Type u_2) [Field F] [IsAlgClosed F] [Ring R] [Algebra F R] [IsSimpleRing R] [FiniteDimensional F R] : ∃ (n : ℕ) (_ : NeZero n), Nonempty (R ≃ₐ[F] Matrix (Fin n) (Fin n) F)

The Wedderburn–Artin Theorem over algebraically closed fields: a finite-dimensional simple algebra over an algebraically closed field is isomorphic to a matrix algebra over the field.

theorem IsSemisimpleRing.exists_algEquiv_pi_matrix_of_isAlgClosed (F : Type u_1) (R : Type u_2) [Field F] [IsAlgClosed F] [Ring R] [Algebra F R] [IsSemisimpleRing R] [FiniteDimensional F R] : ∃ (n : ℕ) (d : Fin n → ℕ), (∀ (i : Fin n), NeZero (d i)) ∧ Nonempty (R ≃ₐ[F] (i : Fin n) → Matrix (Fin (d i)) (Fin (d i)) F)

The Wedderburn–Artin Theorem over algebraically closed fields: a finite-dimensional semisimple algebra over an algebraically closed field is isomorphic to a product of matrix algebras over the field.