feat(algebra/module/basic): More general smul_ne_zero (#16608)

Prove the one way implication of `smul_ne_zero` that holds without `smul_eq_zero` separately. Call it `smul_ne_zero` and rename `smul_ne_zero` to `smul_ne_zero_iff`.

This matches `mul_ne_zero` and `mul_ne_zero_iff`.

src/algebra/module/basic.lean

@@ -512,19 +512,23 @@ instance no_zero_divisors.to_no_zero_smul_divisors [has_zero R] [has_mul R] [no_
   no_zero_smul_divisors R R :=
 ⟨λ c x, eq_zero_or_eq_zero_of_mul_eq_zero⟩
 
-section module
+lemma smul_ne_zero [has_zero R] [has_zero M] [has_smul R M] [no_zero_smul_divisors R M] {c : R}
+  {x : M} (hc : c ≠ 0) (hx : x ≠ 0) : c • x ≠ 0 :=
+λ h, (eq_zero_or_eq_zero_of_smul_eq_zero h).elim hc hx
 
-variables [semiring R] [add_comm_monoid M] [module R M]
+section smul_with_zero
+variables [has_zero R] [has_zero M] [smul_with_zero R M] [no_zero_smul_divisors R M] {c : R} {x : M}
 
-@[simp]
-theorem smul_eq_zero [no_zero_smul_divisors R M] {c : R} {x : M} :
-  c • x = 0 ↔ c = 0 ∨ x = 0 :=
+@[simp] lemma smul_eq_zero : c • x = 0 ↔ c = 0 ∨ x = 0 :=
 ⟨eq_zero_or_eq_zero_of_smul_eq_zero,
- λ h, h.elim (λ h, h.symm ▸ zero_smul R x) (λ h, h.symm ▸ smul_zero c)⟩
+  λ h, h.elim (λ h, h.symm ▸ zero_smul R x) (λ h, h.symm ▸ smul_zero c)⟩
+
+lemma smul_ne_zero_iff : c • x ≠ 0 ↔ c ≠ 0 ∧ x ≠ 0 := by rw [ne.def, smul_eq_zero, not_or_distrib]
 
-theorem smul_ne_zero [no_zero_smul_divisors R M] {c : R} {x : M} :
-  c • x ≠ 0 ↔ c ≠ 0 ∧ x ≠ 0 :=
-by simp only [ne.def, smul_eq_zero, not_or_distrib]
+end smul_with_zero
+
+section module
+variables [semiring R] [add_comm_monoid M] [module R M]
 
 section nat
 

src/algebra/support.lean

@@ -198,9 +198,14 @@ mul_support_binop_subset (/) one_div_one f g
 
 end division_monoid
 
+lemma support_smul [has_zero R] [has_zero M] [smul_with_zero R M] [no_zero_smul_divisors R M]
+  (f : α → R) (g : α → M) :
+  support (f • g) = support f ∩ support g :=
+ext $ λ x, smul_ne_zero_iff
+
 @[simp] lemma support_mul [mul_zero_class R] [no_zero_divisors R] (f g : α → R) :
   support (λ x, f x * g x) = support f ∩ support g :=
-set.ext $ λ x, by simp only [mem_support, mul_ne_zero_iff, mem_inter_iff, not_or_distrib]
+support_smul f g
 
 @[simp] lemma support_mul_subset_left [mul_zero_class R] (f g : α → R) :
   support (λ x, f x * g x) ⊆ support f :=
@@ -220,11 +225,6 @@ lemma support_smul_subset_left [has_zero M] [has_zero β] [smul_with_zero M β]
   support (f • g) ⊆ support f :=
 λ x hfg hf, hfg $ by rw [pi.smul_apply', hf, zero_smul]
 
-lemma support_smul [semiring R] [add_comm_monoid M] [module R M]
-  [no_zero_smul_divisors R M] (f : α → R) (g : α → M) :
-  support (f • g) = support f ∩ support g :=
-ext $ λ x, smul_ne_zero
-
 lemma support_const_smul_of_ne_zero [semiring R] [add_comm_monoid M] [module R M]
   [no_zero_smul_divisors R M] (c : R) (g : α → M) (hc : c ≠ 0) :
   support (c • g) = support g :=

src/geometry/euclidean/oriented_angle.lean

@@ -333,7 +333,7 @@ begin
     by_cases hx : x = 0, { simp [hx] },
     rcases lt_trichotomy r 0 with hr|hr|hr,
     { rw ←neg_smul,
-      exact or.inr ⟨hx, smul_ne_zero.2 ⟨hr.ne, hx⟩,
+      exact or.inr ⟨hx, smul_ne_zero hr.ne hx,
                     same_ray_pos_smul_right x (left.neg_pos_iff.2 hr)⟩ },
     { simp [hr] },
     { exact or.inl (same_ray_pos_smul_right x hr) } }