Section 5 : An introduction to group theory =========================================== Overview of the sheets ---------------------- Lean has a bunch of group theory already (Sylow's theorems, nilpotent and solvable groups and other "final year undergraduate level mathematics"). Should we use what is already there, or rebuild from scratch? In sheet 1 of section 5 we go through a brief tour of how to use Lean's groups. In sheet 2 we make new "class"es ``WeakGroup`` and ``BadGroup`` (so now you can guess how to make groups), and show that a ``WeakGroup`` is the same as a ``Group`` but that there are ``BadGroup`` s which aren't groups. In sheet 3 we give a brief overview of subgroups and group homomorphisms. Structures and classes ---------------------- Groups, subgroups, and group homomorphisms in Lean are all encoded via inductive types. These inductive types are of a particular boring nature: they only have one constructor. Thus in contrast to ``P ∨ Q``, which can be proved in two ways (you either prove ``P`` or you prove ``Q``), there is only one way to make a subgroup of a group: you have to give a subset of the group, plus proofs that it satisfies the axioms of a subgroup. You can read about the details of :ref:`structures ` and :ref:`classes ` by following those links; I will not say any more about them here. What you need to know to do the sheets -------------------------------------- Sheet 1: There will be a lot of ``rw`` involved, because we are constantly using the group axioms. Sheet 2 is perhaps mathematically tricky. Sheet 3 is ``refine`` and ``ext`` and ``apply`` practice.