**This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.**

### Abstract

The focus of this case study is re-use in abstract algebra. It
contains locale-based formalisations of selected parts of set, group
and ring theory from Jacobson's

*Basic Algebra*leading to the respective fundamental homomorphism theorems. The study is not intended as a library base for abstract algebra. It rather explores an approach towards abstract algebra in Isabelle.