/group_theory

group theory done in lean using Dummit and Foote's "Abstract Algebra"

Primary LanguageLean

Group Theory

In order to advance my understanding of group theory, I am writing down and proving the first couple of chapters of Dummit and Foote's "Abstract Algebra" textbook in the automated theorem prover Lean.

So far, here are all the things I have formalized

  • the definition of a group
  • the defintiion of an abelian group
  • propositions about groups, e.g. for all a, -(-a) = a
  • proof that integers under additon are a group
  • proof that rationals under addition are a group
  • proof that the dihedral group is a group
  • proof that the symmetric group is a group
  • defintion of a homomorphism
  • definition of an isomorphism

I welcome all pull requests.