feat: c • x = 0 ↔ c = 0 and similar lemmas (#9390)

and rename and generalise `smul_eq_zero_iff_eq'`/`smul_ne_zero_iff_ne'`

From LeanAPAP

Author: YaelDillies

Mathlib/Algebra/Module/Basic.lean

@@ -586,6 +586,13 @@ theorem smul_eq_zero : c • x = 0 ↔ c = 0 ∨ x = 0 :=
 theorem smul_ne_zero_iff : c • x ≠ 0 ↔ c ≠ 0 ∧ x ≠ 0 := by rw [Ne.def, smul_eq_zero, not_or]
 #align smul_ne_zero_iff smul_ne_zero_iff
 
+lemma smul_eq_zero_iff_left (hx : x ≠ 0) : c • x = 0 ↔ c = 0 := by simp [hx]
+lemma smul_eq_zero_iff_right (hc : c ≠ 0) : c • x = 0 ↔ x = 0 := by simp [hc]
+#align smul_eq_zero_iff_eq' smul_eq_zero_iff_right
+lemma smul_ne_zero_iff_left (hx : x ≠ 0) : c • x ≠ 0 ↔ c ≠ 0 := by simp [hx]
+lemma smul_ne_zero_iff_right (hc : c ≠ 0) : c • x ≠ 0 ↔ x ≠ 0 := by simp [hc]
+#align smul_ne_zero_iff_ne' smul_ne_zero_iff_right
+
 end SMulWithZero
 
 section Module
@@ -720,7 +727,7 @@ variable [GroupWithZero R] [AddMonoid M] [DistribMulAction R M]
 -- see note [lower instance priority]
 /-- This instance applies to `DivisionSemiring`s, in particular `NNReal` and `NNRat`. -/
 instance (priority := 100) GroupWithZero.toNoZeroSMulDivisors : NoZeroSMulDivisors R M :=
-  ⟨fun {_ _} h => or_iff_not_imp_left.2 fun hc => (smul_eq_zero_iff_eq' hc).1 h⟩
+  ⟨fun {a _} h ↦ or_iff_not_imp_left.2 fun ha ↦ (smul_eq_zero_iff_eq $ Units.mk0 a ha).1 h⟩
 #align group_with_zero.to_no_zero_smul_divisors GroupWithZero.toNoZeroSMulDivisors
 
 end GroupWithZero

Mathlib/GroupTheory/GroupAction/Group.lean

@@ -294,20 +294,6 @@ theorem smul_ne_zero_iff_ne (a : α) {x : β} : a • x ≠ 0 ↔ x ≠ 0 :=
 
 end Group
 
-section Gwz
-
-variable [GroupWithZero α] [AddMonoid β] [DistribMulAction α β]
-
-theorem smul_eq_zero_iff_eq' {a : α} (ha : a ≠ 0) {x : β} : a • x = 0 ↔ x = 0 :=
-  show Units.mk0 a ha • x = 0 ↔ x = 0 from smul_eq_zero_iff_eq _
-#align smul_eq_zero_iff_eq' smul_eq_zero_iff_eq'
-
-theorem smul_ne_zero_iff_ne' {a : α} (ha : a ≠ 0) {x : β} : a • x ≠ 0 ↔ x ≠ 0 :=
-  show Units.mk0 a ha • x ≠ 0 ↔ x ≠ 0 from smul_ne_zero_iff_ne _
-#align smul_ne_zero_iff_ne' smul_ne_zero_iff_ne'
-
-end Gwz
-
 end DistribMulAction
 
 section MulDistribMulAction

Mathlib/NumberTheory/NumberField/CanonicalEmbedding.lean

@@ -576,8 +576,8 @@ theorem convexBodySumFun_eq_zero_iff (x : E K) :
       Finset.sum_eq_zero_iff_of_nonneg (fun _ _ => norm_nonneg _)] at h
     ext : 2
     · exact norm_eq_zero.mp (h.1 _ (Finset.mem_univ _))
-    · exact norm_eq_zero.mp ((smul_eq_zero_iff_eq' two_ne_zero (α := ℝ)).mp
-        (h.2 _ (Finset.mem_univ _)))
+    · exact norm_eq_zero.1 $ eq_zero_of_ne_zero_of_mul_left_eq_zero two_ne_zero $ h.2 _ $
+        Finset.mem_univ _
   · simp only [convexBodySumFun, h, Prod.fst_zero, Pi.zero_apply, norm_zero, Finset.sum_const_zero,
       Prod.snd_zero, mul_zero, add_zero]