This is an unofficial reimagining of the Archive of Formal Proofs
Separation Algebraby Gerwin Klein, Rafal Kolanski and Andrew Boyton