Theorems · Theorem · ring theory

IsSimpleRing.exists_algEquiv_matrix_divisionRing

• 1000+ list: Artin–Wedderburn theorem

∀ (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), ∃ D x x_1, Nonempty (R ≃ₐ[R₀] Matrix (Fin n) (Fin n) D)

The Wedderburn–Artin Theorem, algebra form: an Artinian simple algebra is isomorphic to a matrix algebra over a division algebra.

Defined in

Mathlib.RingTheory.SimpleModule.WedderburnArtin

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommSemiringRingAlgebraIsSimpleRingIsArtinianRing