chore(analysis,topology): replace noncomputable theory with `noncom…

…putable` (#16552)


The purpose of this change is to make it easier to parse the diff of a future PR that makes a significant fraction of these definitions computable.

src/analysis/normed/field/basic.lean

@@ -17,7 +17,6 @@ definitions.
 
 variables {α : Type*} {β : Type*} {γ : Type*} {ι : Type*}
 
-noncomputable theory
 open filter metric
 open_locale topological_space big_operators nnreal ennreal uniformity pointwise
 
@@ -185,7 +184,7 @@ instance : non_unital_semi_normed_ring (ulift α) :=
 
 /-- Non-unital seminormed ring structure on the product of two non-unital seminormed rings,
   using the sup norm. -/
-instance prod.non_unital_semi_normed_ring [non_unital_semi_normed_ring β] :
+noncomputable instance prod.non_unital_semi_normed_ring [non_unital_semi_normed_ring β] :
   non_unital_semi_normed_ring (α × β) :=
 { norm_mul := assume x y,
   calc
@@ -202,7 +201,7 @@ instance prod.non_unital_semi_normed_ring [non_unital_semi_normed_ring β] :
 
 /-- Non-unital seminormed ring structure on the product of finitely many non-unital seminormed
 rings, using the sup norm. -/
-instance pi.non_unital_semi_normed_ring {π : ι → Type*} [fintype ι]
+noncomputable instance pi.non_unital_semi_normed_ring {π : ι → Type*} [fintype ι]
   [Π i, non_unital_semi_normed_ring (π i)] :
   non_unital_semi_normed_ring (Π i, π i) :=
 { norm_mul := λ x y, nnreal.coe_mono $
@@ -315,14 +314,15 @@ instance : semi_normed_ring (ulift α) :=
 
 /-- Seminormed ring structure on the product of two seminormed rings,
   using the sup norm. -/
-instance prod.semi_normed_ring [semi_normed_ring β] :
+noncomputable instance prod.semi_normed_ring [semi_normed_ring β] :
   semi_normed_ring (α × β) :=
 { ..prod.non_unital_semi_normed_ring,
   ..prod.seminormed_add_comm_group, }
 
 /-- Seminormed ring structure on the product of finitely many seminormed rings,
   using the sup norm. -/
-instance pi.semi_normed_ring {π : ι → Type*} [fintype ι] [Π i, semi_normed_ring (π i)] :
+noncomputable instance pi.semi_normed_ring {π : ι → Type*} [fintype ι]
+  [Π i, semi_normed_ring (π i)] :
   semi_normed_ring (Π i, π i) :=
 { ..pi.non_unital_semi_normed_ring,
   ..pi.seminormed_add_comm_group, }
@@ -338,13 +338,15 @@ instance : non_unital_normed_ring (ulift α) :=
 
 /-- Non-unital normed ring structure on the product of two non-unital normed rings,
 using the sup norm. -/
-instance prod.non_unital_normed_ring [non_unital_normed_ring β] : non_unital_normed_ring (α × β) :=
+noncomputable instance prod.non_unital_normed_ring [non_unital_normed_ring β] :
+  non_unital_normed_ring (α × β) :=
 { norm_mul := norm_mul_le,
   ..prod.seminormed_add_comm_group }
 
 /-- Normed ring structure on the product of finitely many non-unital normed rings, using the sup
 norm. -/
-instance pi.non_unital_normed_ring {π : ι → Type*} [fintype ι] [Π i, non_unital_normed_ring (π i)] :
+noncomputable instance pi.non_unital_normed_ring {π : ι → Type*} [fintype ι]
+  [Π i, non_unital_normed_ring (π i)] :
   non_unital_normed_ring (Π i, π i) :=
 { norm_mul := norm_mul_le,
   ..pi.normed_add_comm_group }
@@ -366,12 +368,12 @@ instance : normed_ring (ulift α) :=
   .. ulift.normed_add_comm_group }
 
 /-- Normed ring structure on the product of two normed rings, using the sup norm. -/
-instance prod.normed_ring [normed_ring β] : normed_ring (α × β) :=
+noncomputable instance prod.normed_ring [normed_ring β] : normed_ring (α × β) :=
 { norm_mul := norm_mul_le,
   ..prod.normed_add_comm_group }
 
 /-- Normed ring structure on the product of finitely many normed rings, using the sup norm. -/
-instance pi.normed_ring {π : ι → Type*} [fintype ι] [Π i, normed_ring (π i)] :
+noncomputable instance pi.normed_ring {π : ι → Type*} [fintype ι] [Π i, normed_ring (π i)] :
   normed_ring (Π i, π i) :=
 { norm_mul := norm_mul_le,
   ..pi.normed_add_comm_group }
@@ -616,11 +618,11 @@ end densely
 
 end normed_field
 
-instance : normed_field ℝ :=
+noncomputable instance : normed_field ℝ :=
 { norm_mul' := abs_mul,
   .. real.normed_add_comm_group }
 
-instance : densely_normed_field ℝ :=
+noncomputable instance : densely_normed_field ℝ :=
 { lt_norm_lt := λ _ _ h₀ hr, let ⟨x, h⟩ := exists_between hr in
     ⟨x, by rwa [real.norm_eq_abs, abs_of_nonneg (h₀.trans h.1.le)]⟩ }
 
@@ -698,7 +700,7 @@ lemma normed_add_comm_group.tendsto_at_top' [nonempty α] [semilattice_sup α] [
   tendsto f at_top (𝓝 b) ↔ ∀ ε, 0 < ε → ∃ N, ∀ n, N < n → ∥f n - b∥ < ε :=
 (at_top_basis_Ioi.tendsto_iff metric.nhds_basis_ball).trans (by simp [dist_eq_norm])
 
-instance : normed_comm_ring ℤ :=
+noncomputable instance : normed_comm_ring ℤ :=
 { norm := λ n, ∥(n : ℝ)∥,
   norm_mul := λ m n, le_of_eq $ by simp only [norm, int.cast_mul, abs_mul],
   dist_eq := λ m n, by simp only [int.dist_eq, norm, int.cast_sub],
@@ -724,12 +726,12 @@ end
 instance : norm_one_class ℤ :=
 ⟨by simp [← int.norm_cast_real]⟩
 
-instance : normed_field ℚ :=
+noncomputable instance : normed_field ℚ :=
 { norm := λ r, ∥(r : ℝ)∥,
   norm_mul' := λ r₁ r₂, by simp only [norm, rat.cast_mul, abs_mul],
   dist_eq := λ r₁ r₂, by simp only [rat.dist_eq, norm, rat.cast_sub] }
 
-instance : densely_normed_field ℚ :=
+noncomputable instance : densely_normed_field ℚ :=
 { lt_norm_lt := λ r₁ r₂ h₀ hr, let ⟨q, h⟩ := exists_rat_btwn hr in
     ⟨q, by { unfold norm, rwa abs_of_pos (h₀.trans_lt h.1) } ⟩ }
 

src/topology/instances/rat.lean

@@ -13,12 +13,11 @@ import topology.instances.real
 
 The structure of a metric space on `ℚ` is introduced in this file, induced from `ℝ`.
 -/
-noncomputable theory
 open metric set filter
 
 namespace rat
 
-instance : metric_space ℚ :=
+noncomputable instance : metric_space ℚ :=
 metric_space.induced coe rat.cast_injective real.metric_space
 
 theorem dist_eq (x y : ℚ) : dist x y = |x - y| := rfl