refactor(topology/algebra/ring): topological_ring extends `topologi…

…cal_add_group` (#8709)

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 α :=

src/topology/algebra/ring.lean

@@ -86,18 +86,14 @@ 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 α]
 
 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) :=