A Case Study in Basic Algebra

Clemens Ballarin ­čîÉ

August 30, 2019


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.


BSD License


Session Jacobson_Basic_Algebra