From d7fcd8ca11b9a8706f87dc53f1f0ed7a8caec5cc Mon Sep 17 00:00:00 2001
From: "Yury G. Kudryashov" <urkud@urkud.name>
Date: Sun, 26 Jul 2020 07:03:20 +0000
Subject: [PATCH] chore(analysis/normed_space): remove 2 `norm_zero` lemmas
 (#3558)

We have a general `norm_zero` lemma and these lemmas are not used
before we introduce `normed_group` instances.
---
 src/analysis/calculus/mean_value.lean        | 4 ++--
 src/analysis/normed_space/multilinear.lean   | 5 +----
 src/analysis/normed_space/operator_norm.lean | 3 ---
 src/measure_theory/bochner_integration.lean  | 4 ++--
 4 files changed, 5 insertions(+), 11 deletions(-)

diff --git a/src/analysis/calculus/mean_value.lean b/src/analysis/calculus/mean_value.lean
index b47d53a0bc578..27a4be10b7f8c 100644
--- a/src/analysis/calculus/mean_value.lean
+++ b/src/analysis/calculus/mean_value.lean
@@ -367,7 +367,7 @@ begin
     simpa using (has_deriv_at_const x C).mul ((has_deriv_at_id x).sub (has_deriv_at_const x a)) },
   convert image_norm_le_of_norm_deriv_right_le_deriv_boundary hg hg' _ hB bound,
   { simp only [g, B] },
-  { simp only [g, B], rw [sub_self, _root_.norm_zero, sub_self, mul_zero] }
+  { simp only [g, B], rw [sub_self, norm_zero, sub_self, mul_zero] }
 end
 
 /-- A function on `[a, b]` with the norm of the derivative within `[a, b]`
@@ -509,7 +509,7 @@ theorem convex.is_const_of_fderiv_within_eq_zero {s : set E} (hs : convex s)
   {x y : E} (hx : x ∈ s) (hy : y ∈ s) :
   f x = f y :=
 have bound : ∀ x ∈ s, ∥fderiv_within ℝ f s x∥ ≤ 0,
-  from λ x hx, by simp only [hf' x hx, _root_.norm_zero],
+  from λ x hx, by simp only [hf' x hx, norm_zero],
 by simpa only [(dist_eq_norm _ _).symm, zero_mul, dist_le_zero, eq_comm]
   using hs.norm_image_sub_le_of_norm_fderiv_within_le hf bound hx hy
 
diff --git a/src/analysis/normed_space/multilinear.lean b/src/analysis/normed_space/multilinear.lean
index 215cdacd8b096..2ad0ea0defe87 100644
--- a/src/analysis/normed_space/multilinear.lean
+++ b/src/analysis/normed_space/multilinear.lean
@@ -111,7 +111,7 @@ begin
   by a power of a scalar `c` with norm `∥c∥ > 1`.-/
   by_cases h : ∃i, m i = 0,
   { rcases h with ⟨i, hi⟩,
-    rw [f.map_coord_zero i hi, _root_.norm_zero],
+    rw [f.map_coord_zero i hi, norm_zero],
     exact mul_nonneg (le_of_lt C_pos) (prod_nonneg (λi hi, norm_nonneg _)) },
   { push_neg at h,
     have : ∀i, ∃d:𝕜, d ≠ 0 ∧ ∥d • m i∥ ≤ δ ∧ (δ/∥c∥ ≤ ∥d • m i∥) ∧ (∥d∥⁻¹ ≤ δ⁻¹ * ∥c∥ * ∥m i∥) :=
@@ -374,9 +374,6 @@ begin
     simp }
 end
 
-@[simp] lemma norm_zero : ∥(0 : continuous_multilinear_map 𝕜 E₁ E₂)∥ = 0 :=
-by rw op_norm_zero_iff
-
 lemma op_norm_smul_le : ∥c • f∥ ≤ ∥c∥ * ∥f∥ :=
 (Inf_le _ bounds_bdd_below
   ⟨mul_nonneg (norm_nonneg _) (op_norm_nonneg _), λ _,
diff --git a/src/analysis/normed_space/operator_norm.lean b/src/analysis/normed_space/operator_norm.lean
index 91744d66af6fc..f9a628fdfa5e6 100644
--- a/src/analysis/normed_space/operator_norm.lean
+++ b/src/analysis/normed_space/operator_norm.lean
@@ -296,9 +296,6 @@ iff.intro
     ⟨ge_of_eq rfl, λ _, le_of_eq (by { rw [zero_mul, hf], exact norm_zero })⟩)
     (op_norm_nonneg _))
 
-@[simp] lemma norm_zero : ∥(0 : E →L[𝕜] F)∥ = 0 :=
-by rw op_norm_zero_iff
-
 /-- The norm of the identity is at most `1`. It is in fact `1`, except when the space is trivial
 where it is `0`. It means that one can not do better than an inequality in general. -/
 lemma norm_id_le : ∥id 𝕜 E∥ ≤ 1 :=
diff --git a/src/measure_theory/bochner_integration.lean b/src/measure_theory/bochner_integration.lean
index d0a6130821031..c0fa91d5aad68 100644
--- a/src/measure_theory/bochner_integration.lean
+++ b/src/measure_theory/bochner_integration.lean
@@ -1022,7 +1022,7 @@ begin
   by_cases hf : measurable f ∧ integrable f μ,
   { rw [integral_eq f hf.1 hf.2, ← l1.norm_of_fun_eq_lintegral_norm f hf.1 hf.2],
     exact l1.norm_integral_le _ },
-  { rw [integral_undef hf, _root_.norm_zero],
+  { rw [integral_undef hf, norm_zero],
     exact to_real_nonneg }
 end
 
@@ -1197,7 +1197,7 @@ classical.by_cases
     ... = ∫ a, ∥f a∥ ∂μ : (integral_eq_lintegral_of_nonneg_ae le_ae $ measurable.norm h).symm )
 ( λh : ¬measurable f,
   begin
-    rw [integral_non_measurable h, _root_.norm_zero],
+    rw [integral_non_measurable h, norm_zero],
     exact integral_nonneg_of_ae le_ae
   end )