Wedderburn's Little Theorem

This file proves Wedderburn's Little Theorem.

Main Declarations

• littleWedderburn: a finite division ring is a field.

Future work

A couple simple generalisations are possible:

• A finite ring is commutative iff all its nilpotents lie in the center. [Chintala, Vineeth, Sorry, the Nilpotents Are in the Center][chintala2020]
• A ring is commutative if all its elements have finite order. [Dolan, S. W., A Proof of Jacobson's Theorem][dolan1975]

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 littleWedderburn (D : Type u_1) [DivisionRing D] [Finite D] : Field 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 ⋯

def Finite.divisionRing_to_field (D : Type u_1) [DivisionRing D] [Finite D] : Field D

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

• Finite.divisionRing_to_field = littleWedderburn

theorem Finite.isDomain_to_isField (D : Type u_1) [Finite D] [Ring D] [IsDomain D] : IsField D

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