Jacobson_Basic_Algebra swMATH ID: 38027 Software Authors: Clemens Ballarin Description: Jacobson_Basic_Algebra: A Case Study in Basic Algebra. 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. Homepage: https://www.isa-afp.org/entries/Jacobson_Basic_Algebra.html Dependencies: Isabelle Related Software: Automath; Secondary Sylow; Archive Formal Proofs; Locales; Isabelle/HOL; Isabelle; Coq Cited in: 1 Publication Cited by 1 Author 1 Ballarin, Clemens Cited in 1 Serial 1 Journal of Automated Reasoning Cited in 1 Field 1 Computer science (68-XX) Citations by Year