Theorems · Theorem · ring theory

IsSimpleRing.exists_algEquiv_matrix_end_mulOpposite

∀ (R₀ : Type u_1) (R : Type u) [inst : CommSemiring R₀] [inst_1 : Ring R] [inst_2 : Algebra R₀ R] [IsSimpleRing R]
  [IsArtinianRing R],
  ∃ n,
    ∃ (_ : NeZero n), ∃ I, ∃ (_ : IsSimpleModule R ↥I), Nonempty (R ≃ₐ[R₀] Matrix (Fin n) (Fin n) (Module.End R ↥I)ᵐᵒᵖ)

The Wedderburn–Artin Theorem, algebra form: an Artinian simple algebra is isomorphic to a matrix algebra over the opposite of the endomorphism algebra of its simple module.

Defined in

Mathlib.RingTheory.SimpleModule.WedderburnArtin

Cited by

2 results in Mathlib

Foundations

Depth 101 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommSemiringRingAlgebraIsSimpleRingIsArtinianRing