  In this paper we formalize some foundation concepts and theorems of group
theory in a variant of type theory called the Calculus of Constructions with
Definitions. In this theory we introduce definition of a group, which is both
general and simple enough to use in formal proofs. Based on this definition, we
formalize the concepts of subgroup, coset, conjugate, normal subgroup, and
quotient group, and formally derive some related theorems. We aim to keep these
formalizations transparent and concise, and as close as possible to the
standard mathematical theory. The results can be implemented in proof
assistants that are based on calculus of constructions.
