From 5335c67159ea784ed517545082482ef188282822 Mon Sep 17 00:00:00 2001
From: "Yury G. Kudryashov" <urkud@urkud.name>
Date: Wed, 18 Aug 2021 08:28:19 +0000
Subject: [PATCH] refactor(topology/algebra/ring): `topological_ring` extends
 `topological_add_group` (#8709)

---
 src/analysis/normed_space/basic.lean |  5 +----
 src/topology/algebra/ring.lean       | 12 ++++--------
 2 files changed, 5 insertions(+), 12 deletions(-)

diff --git a/src/analysis/normed_space/basic.lean b/src/analysis/normed_space/basic.lean
index 2dbd340f0610c..16b0fbd55f139 100644
--- a/src/analysis/normed_space/basic.lean
+++ b/src/analysis/normed_space/basic.lean
@@ -1181,10 +1181,7 @@ instance semi_normed_ring_top_monoid [semi_normed_ring α] : has_continuous_mul
 
 /-- A seminormed ring is a topological ring. -/
 @[priority 100] -- see Note [lower instance priority]
-instance semi_normed_top_ring [semi_normed_ring α] : topological_ring α :=
-⟨ continuous_iff_continuous_at.2 $ λ x, tendsto_iff_norm_tendsto_zero.2 $
-    have ∀ e : α, -e - -x = -(e - x), by intro; simp,
-    by simp only [this, norm_neg]; apply tendsto_norm_sub_self ⟩
+instance semi_normed_top_ring [semi_normed_ring α] : topological_ring α := { }
 
 /-- A normed field is a field with a norm satisfying ∥x y∥ = ∥x∥ ∥y∥. -/
 class normed_field (α : Type*) extends has_norm α, field α, metric_space α :=
diff --git a/src/topology/algebra/ring.lean b/src/topology/algebra/ring.lean
index 3a8686059224e..5d666760ca3a1 100644
--- a/src/topology/algebra/ring.lean
+++ b/src/topology/algebra/ring.lean
@@ -86,8 +86,7 @@ end
 
 /-- A topological ring is a ring where the ring operations are continuous. -/
 class topological_ring [topological_space α] [ring α]
-  extends has_continuous_add α, has_continuous_mul α : Prop :=
-(continuous_neg : continuous (λa:α, -a))
+  extends topological_add_group α, has_continuous_mul α : Prop
 
 variables {α} [ring α] [topological_space α]
 
@@ -95,9 +94,6 @@ section
 variables [t : topological_ring α]
 @[priority 100] -- see Note [lower instance priority]
 instance topological_ring.to_topological_semiring : topological_semiring α := {..t}
-
-@[priority 100] -- see Note [lower instance priority]
-instance topological_ring.to_topological_add_group : topological_add_group α := {..t}
 end
 
 variables [topological_ring α]
@@ -106,7 +102,7 @@ variables [topological_ring α]
   makes the product into a topological ring. -/
 instance {β : Type*}
   [ring β] [topological_space β] [topological_ring β] : topological_ring (α × β) :=
-{ continuous_neg := continuous_neg }
+{ }
 
 instance {β : Type*} {C : β → Type*} [Π b, topological_space (C b)]
   [Π b, ring (C b)] [∀ b, topological_ring (C b)] : topological_ring (Π b, C b) :=
@@ -124,8 +120,8 @@ continuous_id.mul continuous_const
 itself a subring. -/
 def subring.topological_closure (S : subring α) : subring α :=
 { carrier := closure (S : set α),
-  ..(S.to_submonoid.topological_closure),
-  ..(S.to_add_subgroup.topological_closure) }
+  ..S.to_submonoid.topological_closure,
+  ..S.to_add_subgroup.topological_closure }
 
 instance subring.topological_closure_topological_ring (s : subring α) :
   topological_ring (s.topological_closure) :=