mathlib3

chore(topology/algebra/group_completion): missing namespace

#1518

Merged