mathlib

665cc13c - chore(topology/algebra/group): review (#4570)

chore(topology/algebra/group): review (#4570) * Ensure that we don't use `[topological_group G]` when it suffices to ask for, e.g., `[has_continuous_mul G]`. * Introduce `[has_continuous_sub]`, add an instance for `nnreal`.