English
There exists an isomorphism of rings between a finite Artinian simple ring and a matrix ring over a division ring.
Русский
Существует изоморфизм колец между конечным артиновым простым кольцом и матричной кольцом над делением кольца.
LaTeX
$$$\\exists n, \\exists e : R \\cong \\mathrm{Mat}_{n}(D)$ for some division ring D$$
Lean4
theorem exists_end_algEquiv :
∃ (n : ℕ) (S : Fin n → Submodule R M) (d : Fin n → ℕ),
(∀ i, IsSimpleModule R (S i)) ∧
(∀ i, NeZero (d i)) ∧ Nonempty (End R M ≃ₐ[R₀] Π i, Matrix (Fin (d i)) (Fin (d i)) (End R (S i))) :=
by
choose d pos S _ simple e using fun c : isotypicComponents R M ↦
(IsIsotypic.isotypicComponents c.2).submodule_linearEquiv_fun
classical
exact
⟨_, _, _, fun _ ↦ simple _, fun _ ↦ pos _,
⟨.trans (endAlgEquiv R₀ R M) <|
.trans (.piCongrRight fun c ↦ ((e c).some.algConj R₀).trans (endVecAlgEquivMatrixEnd ..)) <|
(.piCongrLeft' R₀ _ (Finite.equivFin _))⟩⟩
