mathlib3

eb96a25d - feat(topology/algebra/group): extensionality for top group structure