Theorems · Theorem · ring theory

IsSimpleRing.exists_ringEquiv_matrix_end_mulOpposite

∀ (R : Type u) [inst : Ring R] [IsSimpleRing R] [IsArtinianRing R],
  ∃ n, ∃ (_ : NeZero n), ∃ I, ∃ (_ : IsSimpleModule R ↥I), Nonempty (R ≃+* Matrix (Fin n) (Fin n) (Module.End R ↥I)ᵐᵒᵖ)

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

Defined in

Mathlib.RingTheory.SimpleModule.WedderburnArtin

Cited by

1 results in Mathlib

Foundations

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

Assumes

RingIsSimpleRingIsArtinianRing