Commit 2022-05-31 11:57 1eb73395

feat(topology/algebra/group): add continuous_of_continuous_at_one (#14451) This lemma is more general than uniform_continuous_of_continuous_at_one because it allows the codomain to be a monoid.