Email Gateway (Aug 22 2022 at 20:32): Email Gateway (Aug 22 2022 at 20:32):From: Tobias Nipkow <nipkow@in.tum.de>
A Case Study in Basic Algebra
Clemens Ballarin
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.
https://www.isa-afp.org/entries/Jacobson_Basic_Algebra.html
Enjoy!
smime.p7s
Last updated: Apr 25 2024 at 04:18 UTC