feat: port Topology.Algebra.Ring.Basic (#2614)

Mathlib.lean

@@ -1256,6 +1256,7 @@ import Mathlib.Topology.Algebra.Order.MonotoneConvergence
 import Mathlib.Topology.Algebra.Order.ProjIcc
 import Mathlib.Topology.Algebra.Order.T5
 import Mathlib.Topology.Algebra.Order.UpperLower
+import Mathlib.Topology.Algebra.Ring.Basic
 import Mathlib.Topology.Algebra.Semigroup
 import Mathlib.Topology.Algebra.Star
 import Mathlib.Topology.Algebra.UniformGroup

Mathlib/Topology/Algebra/Group/Basic.lean

@@ -878,6 +878,18 @@ theorem continuous_of_continuousAt_one {M hom : Type _} [MulOneClass M] [Topolog
 #align continuous_of_continuous_at_one continuous_of_continuousAt_one
 #align continuous_of_continuous_at_zero continuous_of_continuousAt_zero
 
+@[to_additive continuous_of_continuousAt_zero₂]
+theorem continuous_of_continuousAt_one₂ {H M : Type _} [CommMonoid M] [TopologicalSpace M]
+    [ContinuousMul M] [Group H] [TopologicalSpace H] [TopologicalGroup H] (f : G →* H →* M)
+    (hf : ContinuousAt (fun x : G × H ↦ f x.1 x.2) (1, 1))
+    (hl : ∀ x, ContinuousAt (f x) 1) (hr : ∀ y, ContinuousAt (fun x => f x y) 1) :
+    Continuous (fun x : G × H ↦ f x.1 x.2) := continuous_iff_continuousAt.2 fun (x, y) => by
+  simp only [ContinuousAt, nhds_prod_eq, ← map_mul_left_nhds_one x, ← map_mul_left_nhds_one y,
+    prod_map_map_eq, tendsto_map'_iff, (· ∘ ·), map_mul, MonoidHom.mul_apply] at *
+  refine ((tendsto_const_nhds.mul ((hr y).comp tendsto_fst)).mul
+    (((hl x).comp tendsto_snd).mul hf)).mono_right (le_of_eq ?_)
+  simp only [map_one, mul_one, MonoidHom.one_apply]
+
 @[to_additive]
 theorem TopologicalGroup.ext {G : Type _} [Group G] {t t' : TopologicalSpace G}
     (tg : @TopologicalGroup G t _) (tg' : @TopologicalGroup G t' _)