The file looks good to me. But I think SpecificGroups is meant for constructions/definitions of well-known "specific" (typically finite) groups.

Constructions like quotient groups, products, coproducts, etc... can just go into GroupTheory, I think. So I suggest moving the file one level up.

done

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

• Build
• Check all files imported
• Lint style