English
There exists a decomposition of a semisimple ring into a product of matrix rings over division rings, aligned with its simple components.
Русский
Существует разложение полупрямого кольца на произведение матричных колец над делениями, соответствующее простым компонентам.
LaTeX
$$$\\exists n, D_i, d_i, (\\forall i, D_i \\text{ division ring}) , (\\forall i, Algebra R (D_i)), (\\forall i, NeZero(d_i)) \\Rightarrow R \\cong \\prod_i \\mathrm{Mat}_{d_i}(D_i)$$$
Lean4
/-- The **Wedderburn–Artin Theorem**, algebra form: a semisimple algebra is isomorphic to a
product of matrix algebras over division algebras. -/
theorem exists_algEquiv_pi_matrix_divisionRing :
∃ (n : ℕ) (D : Fin n → Type u) (d : Fin n → ℕ) (_ : ∀ i, DivisionRing (D i)) (_ : ∀ i, Algebra R₀ (D i)),
(∀ i, NeZero (d i)) ∧ Nonempty (R ≃ₐ[R₀] Π i, Matrix (Fin (d i)) (Fin (d i)) (D i)) :=
by
have ⟨n, S, d, _, hd, ⟨e⟩⟩ := exists_algEquiv_pi_matrix_end_mulOpposite R₀ R
classical exact ⟨n, _, d, inferInstance, inferInstance, hd, ⟨e⟩⟩
