This is an unofficial reimagining of the Archive of Formal Proofs
Groups, Rings and Modulesby Hidetsune Kobayashi, L. Chen and H. Murao