English
For a semisimple ring R over an alg closed field F with finite dimension, there exist a finite index n and a family d: Fin n → ℕ with nonzero entries such that R ≃ₐ[F] ∏ i, Matrix(Fin(d(i)), Fin(d(i)), F).
Русский
Для полносемплого кольца R над алгебраически замкнутым полем F размера конечного, существует разложение на произведение матричных алгебр через неотрицательные целые d(i).
LaTeX
$$[IsSemisimpleRing R][FiniteDimensional F R] ⇒ ∃n, d: Fin n → ℕ, (∀ i, d i ≠ 0) ∧ Nonempty (R ≃ₐ[F] Π i, Matrix(Fin(d i), Fin(d i)) F).$$
Lean4
/-- 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 exists_algEquiv_matrix_of_isAlgClosed [IsSimpleRing R] [FiniteDimensional F R] :
∃ (n : ℕ) (_ : NeZero n), Nonempty (R ≃ₐ[F] Matrix (Fin n) (Fin n) F) :=
have := IsArtinianRing.of_finite F R
have ⟨n, hn, D, _, _, _, ⟨e⟩⟩ := exists_algEquiv_matrix_divisionRing_finite F R
⟨n, hn,
⟨e.trans <| .mapMatrix <| .symm <| .ofBijective (Algebra.ofId F D) IsAlgClosed.algebraMap_bijective_of_isIntegral⟩⟩
