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.

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 (_ : ∀ (a : D), a ≠ 0 → a * a⁻¹ = 1) (_ : 0⁻¹ = 0) 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.