chore: delete lemmas about T0 seminormed groups (#19438)

Those duplicate lemmas about normed groups

Author: YaelDillies

Mathlib/Analysis/Distribution/SchwartzSpace.lean

@@ -1172,7 +1172,7 @@ instance instZeroAtInftyContinuousMapClass : ZeroAtInftyContinuousMapClass 𝓢(
     intro x hx
     rw [div_lt_iff₀ hε] at hx
     have hxpos : 0 < ‖x‖ := by
-      rw [norm_pos_iff']
+      rw [norm_pos_iff]
       intro hxzero
       simp only [hxzero, norm_zero, zero_mul, ← not_le] at hx
       exact hx (apply_nonneg (SchwartzMap.seminorm ℝ 1 0) f)

Mathlib/Analysis/InnerProductSpace/Positive.lean

@@ -109,7 +109,7 @@ lemma antilipschitz_of_forall_le_inner_map {H : Type*} [NormedAddCommGroup H]
   simp_rw [sq, mul_assoc] at h
   by_cases hx0 : x = 0
   · simp [hx0]
-  · apply (map_le_map_iff <| OrderIso.mulLeft₀ ‖x‖ (norm_pos_iff'.mpr hx0)).mp
+  · apply (map_le_map_iff <| OrderIso.mulLeft₀ ‖x‖ (norm_pos_iff.mpr hx0)).mp
     exact (h x).trans <| (norm_inner_le_norm _ _).trans <| (mul_comm _ _).le
 
 lemma isUnit_of_forall_le_norm_inner_map (f : E →L[𝕜] E) {c : ℝ≥0} (hc : 0 < c)

Mathlib/Analysis/Normed/Affine/ContinuousAffineMap.lean

@@ -175,7 +175,7 @@ noncomputable instance : NormedAddCommGroup (V →ᴬ[𝕜] W) :=
           simp only [norm_eq_zero, coe_const, Function.const_apply] at h₁
           rw [h₁]
           rfl
-        · rw [norm_eq_zero', contLinear_eq_zero_iff_exists_const] at h₁
+        · rw [norm_eq_zero, contLinear_eq_zero_iff_exists_const] at h₁
           obtain ⟨q, rfl⟩ := h₁
           simp only [norm_le_zero_iff, coe_const, Function.const_apply] at h₂
           rw [h₂]

Mathlib/Analysis/Normed/Group/Basic.lean

@@ -922,20 +922,6 @@ theorem SeminormedCommGroup.mem_closure_iff :
     a ∈ closure s ↔ ∀ ε, 0 < ε → ∃ b ∈ s, ‖a / b‖ < ε := by
   simp [Metric.mem_closure_iff, dist_eq_norm_div]
 
-@[to_additive norm_le_zero_iff']
-theorem norm_le_zero_iff''' [T0Space E] {a : E} : ‖a‖ ≤ 0 ↔ a = 1 := by
-  letI : NormedGroup E :=
-    { ‹SeminormedGroup E› with toMetricSpace := MetricSpace.ofT0PseudoMetricSpace E }
-  rw [← dist_one_right, dist_le_zero]
-
-@[to_additive norm_eq_zero']
-theorem norm_eq_zero''' [T0Space E] {a : E} : ‖a‖ = 0 ↔ a = 1 :=
-  (norm_nonneg' a).le_iff_eq.symm.trans norm_le_zero_iff'''
-
-@[to_additive norm_pos_iff']
-theorem norm_pos_iff''' [T0Space E] {a : E} : 0 < ‖a‖ ↔ a ≠ 1 := by
-  rw [← not_le, norm_le_zero_iff''']
-
 @[to_additive]
 theorem SeminormedGroup.tendstoUniformlyOn_one {f : ι → κ → G} {s : Set κ} {l : Filter ι} :
     TendstoUniformlyOn f 1 l s ↔ ∀ ε > 0, ∀ᶠ i in l, ∀ x ∈ s, ‖f i x‖ < ε := by
@@ -1292,24 +1278,26 @@ section NormedGroup
 
 variable [NormedGroup E] {a b : E}
 
+@[to_additive (attr := simp) norm_le_zero_iff]
+lemma norm_le_zero_iff' : ‖a‖ ≤ 0 ↔ a = 1 := by rw [← dist_one_right, dist_le_zero]
+
+@[to_additive (attr := simp) norm_pos_iff]
+lemma norm_pos_iff' : 0 < ‖a‖ ↔ a ≠ 1 := by rw [← not_le, norm_le_zero_iff']
+
 @[to_additive (attr := simp) norm_eq_zero]
-theorem norm_eq_zero'' : ‖a‖ = 0 ↔ a = 1 :=
-  norm_eq_zero'''
+lemma norm_eq_zero' : ‖a‖ = 0 ↔ a = 1 := (norm_nonneg' a).le_iff_eq.symm.trans norm_le_zero_iff'
 
 @[to_additive norm_ne_zero_iff]
-theorem norm_ne_zero_iff' : ‖a‖ ≠ 0 ↔ a ≠ 1 :=
-  norm_eq_zero''.not
+lemma norm_ne_zero_iff' : ‖a‖ ≠ 0 ↔ a ≠ 1 := norm_eq_zero'.not
 
-@[to_additive (attr := simp) norm_pos_iff]
-theorem norm_pos_iff'' : 0 < ‖a‖ ↔ a ≠ 1 :=
-  norm_pos_iff'''
-
-@[to_additive (attr := simp) norm_le_zero_iff]
-theorem norm_le_zero_iff'' : ‖a‖ ≤ 0 ↔ a = 1 :=
-  norm_le_zero_iff'''
+@[deprecated (since := "2024-11-24")] alias norm_le_zero_iff'' := norm_le_zero_iff'
+@[deprecated (since := "2024-11-24")] alias norm_le_zero_iff''' := norm_le_zero_iff'
+@[deprecated (since := "2024-11-24")] alias norm_pos_iff'' := norm_pos_iff'
+@[deprecated (since := "2024-11-24")] alias norm_eq_zero'' := norm_eq_zero'
+@[deprecated (since := "2024-11-24")] alias norm_eq_zero''' := norm_eq_zero'
 
 @[to_additive]
-theorem norm_div_eq_zero_iff : ‖a / b‖ = 0 ↔ a = b := by rw [norm_eq_zero'', div_eq_one]
+theorem norm_div_eq_zero_iff : ‖a / b‖ = 0 ↔ a = b := by rw [norm_eq_zero', div_eq_one]
 
 @[to_additive]
 theorem norm_div_pos_iff : 0 < ‖a / b‖ ↔ a ≠ b := by
@@ -1318,7 +1306,7 @@ theorem norm_div_pos_iff : 0 < ‖a / b‖ ↔ a ≠ b := by
 
 @[to_additive eq_of_norm_sub_le_zero]
 theorem eq_of_norm_div_le_zero (h : ‖a / b‖ ≤ 0) : a = b := by
-  rwa [← div_eq_one, ← norm_le_zero_iff'']
+  rwa [← div_eq_one, ← norm_le_zero_iff']
 
 alias ⟨eq_of_norm_div_eq_zero, _⟩ := norm_div_eq_zero_iff
 
@@ -1334,7 +1322,7 @@ theorem eq_one_or_nnnorm_pos (a : E) : a = 1 ∨ 0 < ‖a‖₊ :=
 
 @[to_additive (attr := simp) nnnorm_eq_zero]
 theorem nnnorm_eq_zero' : ‖a‖₊ = 0 ↔ a = 1 := by
-  rw [← NNReal.coe_eq_zero, coe_nnnorm', norm_eq_zero'']
+  rw [← NNReal.coe_eq_zero, coe_nnnorm', norm_eq_zero']
 
 @[to_additive nnnorm_ne_zero_iff]
 theorem nnnorm_ne_zero_iff' : ‖a‖₊ ≠ 0 ↔ a ≠ 1 :=
@@ -1346,24 +1334,24 @@ lemma nnnorm_pos' : 0 < ‖a‖₊ ↔ a ≠ 1 := pos_iff_ne_zero.trans nnnorm_n
 /-- See `tendsto_norm_one` for a version with full neighborhoods. -/
 @[to_additive "See `tendsto_norm_zero` for a version with full neighborhoods."]
 lemma tendsto_norm_one' : Tendsto (norm : E → ℝ) (𝓝[≠] 1) (𝓝[>] 0) :=
-  tendsto_norm_one.inf <| tendsto_principal_principal.2 fun _ hx ↦ norm_pos_iff''.2 hx
+  tendsto_norm_one.inf <| tendsto_principal_principal.2 fun _ hx ↦ norm_pos_iff'.2 hx
 
 @[to_additive]
 theorem tendsto_norm_div_self_punctured_nhds (a : E) :
     Tendsto (fun x => ‖x / a‖) (𝓝[≠] a) (𝓝[>] 0) :=
   (tendsto_norm_div_self a).inf <|
-    tendsto_principal_principal.2 fun _x hx => norm_pos_iff''.2 <| div_ne_one.2 hx
+    tendsto_principal_principal.2 fun _x hx => norm_pos_iff'.2 <| div_ne_one.2 hx
 
 @[to_additive]
 theorem tendsto_norm_nhdsWithin_one : Tendsto (norm : E → ℝ) (𝓝[≠] 1) (𝓝[>] 0) :=
-  tendsto_norm_one.inf <| tendsto_principal_principal.2 fun _x => norm_pos_iff''.2
+  tendsto_norm_one.inf <| tendsto_principal_principal.2 fun _x => norm_pos_iff'.2
 
 variable (E)
 
 /-- The norm of a normed group as a group norm. -/
 @[to_additive "The norm of a normed group as an additive group norm."]
 def normGroupNorm : GroupNorm E :=
-  { normGroupSeminorm _ with eq_one_of_map_eq_zero' := fun _ => norm_eq_zero''.1 }
+  { normGroupSeminorm _ with eq_one_of_map_eq_zero' := fun _ => norm_eq_zero'.1 }
 
 @[simp]
 theorem coe_normGroupNorm : ⇑(normGroupNorm E) = norm :=

Mathlib/Analysis/Normed/Group/Uniform.lean

@@ -381,7 +381,7 @@ instance : NormedCommGroup (SeparationQuotient E) where
 
 @[to_additive]
 theorem mk_eq_one_iff {p : E} : mk p = 1 ↔ ‖p‖ = 0 := by
-  rw [← norm_mk', norm_eq_zero'']
+  rw [← norm_mk', norm_eq_zero']
 
 set_option linter.docPrime false in
 @[to_additive (attr := simp) nnnorm_mk]

Mathlib/MeasureTheory/Integral/IntegrableOn.lean

@@ -489,7 +489,7 @@ lemma IntegrableAtFilter.eq_zero_of_tendsto
     (h : IntegrableAtFilter f l μ) (h' : ∀ s ∈ l, μ s = ∞) {a : E}
     (hf : Tendsto f l (𝓝 a)) : a = 0 := by
   by_contra H
-  obtain ⟨ε, εpos, hε⟩ : ∃ (ε : ℝ), 0 < ε ∧ ε < ‖a‖ := exists_between (norm_pos_iff'.mpr H)
+  obtain ⟨ε, εpos, hε⟩ : ∃ (ε : ℝ), 0 < ε ∧ ε < ‖a‖ := exists_between (norm_pos_iff.mpr H)
   rcases h with ⟨u, ul, hu⟩
   let v := u ∩ {b | ε < ‖f b‖}
   have hv : IntegrableOn f v μ := hu.mono_set inter_subset_left

Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean

@@ -367,8 +367,8 @@ theorem forall_normAtPlace_eq_zero_iff {x : mixedSpace K} :
     (∀ w, normAtPlace w x = 0) ↔ x = 0 := by
   refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
   · ext w
-    · exact norm_eq_zero'.mp (normAtPlace_apply_isReal w.prop _ ▸ h w.1)
-    · exact norm_eq_zero'.mp (normAtPlace_apply_isComplex w.prop _ ▸ h w.1)
+    · exact norm_eq_zero.mp (normAtPlace_apply_isReal w.prop _ ▸ h w.1)
+    · exact norm_eq_zero.mp (normAtPlace_apply_isComplex w.prop _ ▸ h w.1)
   · simp_rw [h, map_zero, implies_true]
 
 @[deprecated (since := "2024-09-13")] alias normAtPlace_eq_zero := forall_normAtPlace_eq_zero_iff

scripts/nolints_prime_decls.txt

@@ -3455,21 +3455,24 @@ NormedSpace.isVonNBounded_iff'
 NormedSpace.norm_expSeries_summable'
 NormedSpace.norm_expSeries_summable_of_mem_ball'
 norm_eq_of_mem_sphere'
+norm_eq_zero'
 norm_eq_zero''
 norm_eq_zero'''
 norm_inv'
 norm_le_norm_add_const_of_dist_le'
 norm_le_norm_add_norm_div'
 norm_le_of_mem_closedBall'
 norm_le_pi_norm'
+norm_le_zero_iff'
 norm_le_zero_iff''
 norm_le_zero_iff'''
 norm_lt_of_mem_ball'
 norm_ne_zero_iff'
 norm_nonneg'
 norm_of_subsingleton'
 norm_one'
-norm_pos_iff''
+norm_pos_iff'
+norm_pos_iff'
 norm_pos_iff'''
 norm_sub_norm_le'
 norm_toNNReal'