English
A semisimple ring admits a decomposition into a product of matrix rings over the opposite of endomorphism rings of its simple modules, indexed by a finite set.
Русский
Полупрямое кольцо допускает разложение на произведение матричных колец над противоположных End-колец его простых модулей, индексируемое конечным множеством.
LaTeX
$$$\\exists n, S, d, (\\forall i, IsSimpleModule R (Subtype fun x => \\dots )) \\, \\Rightarrow \\, R \\cong \\prod_i \\mathrm{Mat}_{d_i}( \\mathrm{End}_R(S_i)^{op})$$$
Lean4
/-- The **Wedderburn–Artin Theorem**: a semisimple ring is isomorphic to a
product of matrix rings over the opposite of the endomorphism rings of its simple modules. -/
theorem exists_ringEquiv_pi_matrix_end_mulOpposite :
∃ (n : ℕ) (D : Fin n → Ideal R) (d : Fin n → ℕ),
(∀ i, IsSimpleModule R (D i)) ∧
(∀ i, NeZero (d i)) ∧ Nonempty (R ≃+* Π i, Matrix (Fin (d i)) (Fin (d i)) (Module.End R (D i))ᵐᵒᵖ) :=
have ⟨n, S, d, hS, hd, ⟨e⟩⟩ := exists_algEquiv_pi_matrix_end_mulOpposite ℕ R
⟨n, S, d, hS, hd, ⟨e⟩⟩
