Journal of Formalized Mathematics
Volume 15, 2003
University of Bialystok
Copyright (c) 2003 Association of Mizar Users

## Witt's Proof of the Wedderburn Theorem

Broderic Arneson
Matthias Baaz
Technische Universit\"at Wien, Vienna, Austria
Piotr Rudnicki

### 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.

This work has been supported by NSERC Grant OGP9207.

#### MML Identifier: WEDDWITT

The terminology and notation used in this paper have been introduced in the following articles [21] [31] [23] [7] [12] [24] [3] [25] [14] [32] [5] [6] [4] [8] [28] [16] [9] [15] [2] [29] [18] [10] [27] [13] [1] [17] [26] [30] [33] [19] [22] [20] [11]

#### Contents (PDF format)

1. Preliminaries
2. Class Formula for Groups
3. Centers and Centralizers of Skew Fields
4. Vector Spaces over Centers of Skew Fields
5. Witt's Proof of Wedderburn's Theorem

#### Bibliography

[1] Broderic Arneson and Piotr Rudnicki. Primitive roots of unity and cyclotomic polynomials. Journal of Formalized Mathematics, 15, 2003.
[2] Grzegorz Bancerek. Cardinal numbers. Journal of Formalized Mathematics, 1, 1989.
[3] Grzegorz Bancerek. The fundamental properties of natural numbers. Journal of Formalized Mathematics, 1, 1989.
[4] Grzegorz Bancerek and Krzysztof Hryniewiecki. Segments of natural numbers and finite sequences. Journal of Formalized Mathematics, 1, 1989.
[5] Czeslaw Bylinski. Functions and their basic properties. Journal of Formalized Mathematics, 1, 1989.
[6] Czeslaw Bylinski. Functions from a set to a set. Journal of Formalized Mathematics, 1, 1989.
[7] Czeslaw Bylinski. Some basic properties of sets. Journal of Formalized Mathematics, 1, 1989.
[8] Czeslaw Bylinski. Finite sequences and tuples of elements of a non-empty sets. Journal of Formalized Mathematics, 2, 1990.
[9] Czeslaw Bylinski. The sum and product of finite sequences of real numbers. Journal of Formalized Mathematics, 2, 1990.
[10] Agata Darmochwal. Finite sets. Journal of Formalized Mathematics, 1, 1989.
[11] Yoshinori Fujisawa, Yasushi Fuwa, and Hidetaka Shimizu. Euler's Theorem and small Fermat's Theorem. Journal of Formalized Mathematics, 10, 1998.
[12] Krzysztof Hryniewiecki. Basic properties of real numbers. Journal of Formalized Mathematics, 1, 1989.
[13] Andrzej Kondracki. The Chinese Remainder Theorem. Journal of Formalized Mathematics, 9, 1997.
[14] Eugeniusz Kusak, Wojciech Leonczuk, and Michal Muzalewski. Abelian groups, fields and vector spaces. Journal of Formalized Mathematics, 1, 1989.
[15] Anna Justyna Milewska. The field of complex numbers. Journal of Formalized Mathematics, 12, 2000.
[16] Takaya Nishiyama and Yasuho Mizuhara. Binary arithmetics. Journal of Formalized Mathematics, 5, 1993.
[17] Beata Padlewska. Families of sets. Journal of Formalized Mathematics, 1, 1989.
[18] Konrad Raczkowski. Integer and rational exponents. Journal of Formalized Mathematics, 2, 1990.
[19] Konrad Raczkowski and Pawel Sadowski. Equivalence relations and classes of abstraction. Journal of Formalized Mathematics, 1, 1989.
[20] Andrzej Trybulec. Binary operations applied to functions. Journal of Formalized Mathematics, 1, 1989.
[21] Andrzej Trybulec. Tarski Grothendieck set theory. Journal of Formalized Mathematics, Axiomatics, 1989.
[22] Andrzej Trybulec. Function domains and Fr\aenkel operator. Journal of Formalized Mathematics, 2, 1990.
[23] Andrzej Trybulec. Subsets of real numbers. Journal of Formalized Mathematics, Addenda, 2003.
[24] Michal J. Trybulec. Integers. Journal of Formalized Mathematics, 2, 1990.
[25] Wojciech A. Trybulec. Vectors in real linear space. Journal of Formalized Mathematics, 1, 1989.
[26] Wojciech A. Trybulec. Classes of conjugation. Normal subgroups. Journal of Formalized Mathematics, 2, 1990.
[27] Wojciech A. Trybulec. Groups. Journal of Formalized Mathematics, 2, 1990.
[28] Wojciech A. Trybulec. Pigeon hole principle. Journal of Formalized Mathematics, 2, 1990.
[29] Wojciech A. Trybulec. Subgroup and cosets of subgroups. Journal of Formalized Mathematics, 2, 1990.
[30] Wojciech A. Trybulec. Commutator and center of a group. Journal of Formalized Mathematics, 3, 1991.
[31] Zinaida Trybulec. Properties of subsets. Journal of Formalized Mathematics, 1, 1989.
[32] Edmund Woronowicz. Relations and their basic properties. Journal of Formalized Mathematics, 1, 1989.
[33] Mariusz Zynel. The Steinitz theorem and the dimension of a vector space. Journal of Formalized Mathematics, 7, 1995.