Documentation

Mathlib.RingTheory.LittleWedderburn

Wedderburn's Little Theorem #

This file proves Wedderburn's Little Theorem.

Main Declarations #

Future work #

A couple simple generalisations are possible:

When alternativity is added to Mathlib, one could formalise the Artin-Zorn theorem, which states that any finite alternative division ring is in fact a field. https://en.wikipedia.org/wiki/Artin%E2%80%93Zorn_theorem

If interested, generalisations to semifields could be explored. The theory of semi-vector spaces is not clear, but assuming that such a theory could be found where every module considered in the below proof is free, then the proof works nearly verbatim.

Everything in this namespace is internal to the proof of Wedderburn's little theorem.

@[instance 100]
instance littleWedderburn (D : Type u_1) [DivisionRing D] [Finite D] :

A finite division ring is a field. See Finite.isDomain_to_isField and Fintype.divisionRingOfIsDomain for more general statements, but these create data, and therefore may cause diamonds if used improperly.

Equations
  • littleWedderburn D = let __src := inst✝; Field.mk DivisionRing.zpow DivisionRing.nnqsmul DivisionRing.qsmul

Alias of littleWedderburn.


A finite division ring is a field. See Finite.isDomain_to_isField and Fintype.divisionRingOfIsDomain for more general statements, but these create data, and therefore may cause diamonds if used improperly.

Equations
Instances For
    theorem Finite.isDomain_to_isField (D : Type u_1) [Finite D] [Ring D] [IsDomain D] :

    A finite domain is a field. See also littleWedderburn and Fintype.divisionRingOfIsDomain.