Witt's Proof of the Wedderburn Theorem

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: University of Alberta, Edmonton, Canada
Matthias Baaz: Technische Universit\"at Wien, Vienna, Austria
Piotr Rudnicki: University of Alberta, Edmonton, Canada

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)

Preliminaries
Class Formula for Groups
Centers and Centralizers of Skew Fields
Vector Spaces over Centers of Skew Fields
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.

Received December 30, 2003

[ Download a postscript version, MML identifier index, Mizar home page]