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] [IsSimpleRing R] [Algebra F R] [FiniteDimensional F R] : ∃ (n : ℕ) (_ : NeZero n), Nonempty (R ≃ₐ[F] Matrix (Fin n) (Fin n) F)