Volume 15, 2003

University of Bialystok

Copyright (c) 2003 Association of Mizar Users

**Broderic Arneson**- University of Alberta, Edmonton, Canada
**Matthias Baaz**- Technische Universit\"at Wien, Vienna, Austria
**Piotr Rudnicki**- University of Alberta, Edmonton, Canada

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

- 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

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

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