isSemisimpleRing_iff_pi_matrix_divisionRing

Mathlib.RingTheory.SimpleModule.Basic

URI: https://scilib.ai/kg/mathlib#isSemisimpleRing_iff_pi_matrix_divisionRing

Lean4

/-- The existence part of the Artin–Wedderburn theorem. -/
axiom isSemisimpleRing_iff_pi_matrix_divisionRing {R : Type u} [Ring R] :
    IsSemisimpleRing R ↔
      ∃ (n : ℕ) (S : Fin n → Type u) (d : Fin n → ℕ) (_ : Π i, DivisionRing (S i)),
        Nonempty (R ≃+* Π i, Matrix (Fin (d i)) (Fin (d i)) (S i))

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru