feat(topology/algebra): uniform continuity from 0 (#7318)

From https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/Linear.20map.20is.20continuous.20if.20it's.20continuous.20at.20zero/near/234714207, thanks to @PatrickMassot.

src/topology/algebra/uniform_group.lean

@@ -132,6 +132,12 @@ begin
   exact tendsto.comp h tendsto_comap
 end
 
+lemma add_monoid_hom.uniform_continuous_of_continuous_at_zero
+  [uniform_space β] [add_group β] [uniform_add_group β]
+  (f : α →+ β) (hf : continuous_at f 0) :
+  uniform_continuous f :=
+uniform_continuous_of_tendsto_zero (by simpa using hf.tendsto)
+
 lemma uniform_continuous_of_continuous [uniform_space β] [add_group β] [uniform_add_group β]
   {f : α → β} [is_add_group_hom f] (h : continuous f) :
   uniform_continuous f :=