@MISC{WEDDWITT.MIZ,
  AUTHOR = {Arneson, Broderick and Baaz, Matthias and Rudnicki, Piotr},
  TITLE = {Witt's Proof of the {W}edderburn Theorem},
  NOTE = {This work has been supported by NSERC Grant OGP9207.},
  SECTION1 = {Preliminaries},
  SECTION2 = {Class Formula for Groups},
  SECTION3 = {Centers and Centralizers of Skew Fields},
  SECTION4 = {Vector Spaces over Centers of Skew Fields},
  SECTION5 = {Witt's Proof of Wedderburn's Theorem},
  DAY = {30},
  MONTH = {December},
  YEAR = {2003},
  ADDRESS1 = {University of Alberta\\Edmonton},
  ADDRESS2 = {Technische Universit\"{a}t Wien},
  ADDRESS3 = {University of Alberta\\Edmonton},
  SUMMARY = {We present a formalization of Witt's proof of the
Wedderburn theorem
  following Chapter 5 of {\em Proofs from THE BOOK} by
  Martin Aigner and G\"{u}nter M. Ziegler, 2nd ed., Springer 1999.}}

