refactor(library/algebra/group): rename theorems, add example