exists_ringEquiv_matrix_divisionRing

English

The supremum of all isotypic components equals the top submodule.

Русский

Наибольший супремум всех изотипических компонент равен верхнему подмодулю.

LaTeX

$$$\\bigvee\\mathrm{isotypicComponents}\\; R\\; M = \\top$$$

Lean4

/-- The **Wedderburn–Artin Theorem**: an Artinian simple ring is isomorphic to a matrix
ring over a division ring. -/
theorem exists_ringEquiv_matrix_divisionRing :
    ∃ (n : ℕ) (_ : NeZero n) (D : Type u) (_ : DivisionRing D), Nonempty (R ≃+* Matrix (Fin n) (Fin n) D) :=
  by
  have ⟨n, hn, I, _, ⟨e⟩⟩ := exists_ringEquiv_matrix_end_mulOpposite R
  classical exact ⟨n, hn, _, _, ⟨e⟩⟩

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