exists_ringEquiv_pi_matrix_divisionRing

English

In the finite case, a finite semisimple ring is isomorphic to a product of matrix rings over finite division rings.

Русский

В конечном случае конечное полупрямое кольцо изоморфно произведению матричных колец над конечными делением кольца.

LaTeX

$$$[Module.Finite\\;R_0\\;R] \\,\\Rightarrow \\, \\exists n, D_i, d_i \\, (\\text{division ring } D_i) \\, \\land \\, R \\cong \\prod_i \\mathrm{Mat}_{d_i}(D_i)$$$

Lean4

/-- The **Wedderburn–Artin Theorem**: a semisimple ring is isomorphic to a
product of matrix rings over division rings. -/
theorem exists_ringEquiv_pi_matrix_divisionRing :
    ∃ (n : ℕ) (D : Fin n → Type u) (d : Fin n → ℕ) (_ : ∀ i, DivisionRing (D i)),
      (∀ i, NeZero (d i)) ∧ Nonempty (R ≃+* Π i, Matrix (Fin (d i)) (Fin (d i)) (D i)) :=
  have ⟨n, D, d, _, _, hd, ⟨e⟩⟩ := exists_algEquiv_pi_matrix_divisionRing ℕ R
  ⟨n, D, d, _, hd, ⟨e⟩⟩

Похожие утверждения