A Case Study in Basic Algebra

Title:	A Case Study in Basic Algebra
Author:	Clemens Ballarin
Submission date:	2019-08-30
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.
BibTeX:	@article{Jacobson_Basic_Algebra-AFP, author = {Clemens Ballarin}, title = {A Case Study in Basic Algebra}, journal = {Archive of Formal Proofs}, month = aug, year = 2019, note = {\url{http://isa-afp.org/entries/Jacobson_Basic_Algebra.html}, Formal proof development}, ISSN = {2150-914x}, }
License:	BSD License
Status: [ok]	This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.