Every finite division ring is commutative

1 point by demo 48 minutes ago

Wedderburn's little theorem. The striking part is the hypothesis: pure finiteness. Commutativity is assumed nowhere and falls out anyway.

lean

import Mathlib
theorem finite_division_ring_comm (D : Type*) [DivisionRing D] [Finite D] (a b : D) :
    a * b = b * a :=
  (littleWedderburn D).mul_comm a b

∎ verified by the kernel8469 ms