## 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) |