From fb41da97816e716c002c723f7f08e103874d9f50 Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpvdoorn@gmail.com>
Date: Thu, 10 Feb 2022 20:44:00 +0000
Subject: [PATCH] feat(algebra/module/basic): turn implications into iffs
 (#11937)

* Turn the following implications into `iff`, rename them accordingly, and make the type arguments explicit (`M` has to be explicit when using it in `rw`, otherwise one will have unsolved type-class arguments)
```
eq_zero_of_two_nsmul_eq_zero -> two_nsmul_eq_zero
eq_zero_of_eq_neg -> self_eq_neg
ne_neg_of_ne_zero -> self_ne_neg
```
* Also add two variants
* Generalize `ne_neg_iff_ne_zero` to work in modules over a ring
---
 src/algebra/module/basic.lean            | 35 ++++++++++--------------
 src/analysis/normed_space/basic.lean     |  2 +-
 src/measure_theory/integral/bochner.lean |  4 +--
 3 files changed, 17 insertions(+), 24 deletions(-)

diff --git a/src/algebra/module/basic.lean b/src/algebra/module/basic.lean
index 1282f21866934..3ea2779d74ada 100644
--- a/src/algebra/module/basic.lean
+++ b/src/algebra/module/basic.lean
@@ -521,11 +521,8 @@ include R
 lemma nat.no_zero_smul_divisors : no_zero_smul_divisors ℕ M :=
 ⟨by { intros c x, rw [nsmul_eq_smul_cast R, smul_eq_zero], simp }⟩
 
-variables {M}
-
-lemma eq_zero_of_two_nsmul_eq_zero {v : M} (hv : 2 • v = 0) : v = 0 :=
-by haveI := nat.no_zero_smul_divisors R M;
-exact (smul_eq_zero.mp hv).resolve_left (by norm_num)
+@[simp] lemma two_nsmul_eq_zero {v : M} : 2 • v = 0 ↔ v = 0 :=
+by { haveI := nat.no_zero_smul_divisors R M, norm_num [smul_eq_zero] }
 
 end nat
 
@@ -559,15 +556,20 @@ end smul_injective
 
 section nat
 
-variables (R) [no_zero_smul_divisors R M] [char_zero R]
+variables (R M) [no_zero_smul_divisors R M] [char_zero R]
 include R
 
-lemma eq_zero_of_eq_neg {v : M} (hv : v = - v) : v = 0 :=
-begin
-  refine eq_zero_of_two_nsmul_eq_zero R _,
-  rw two_smul,
-  exact add_eq_zero_iff_eq_neg.mpr hv
-end
+lemma self_eq_neg {v : M} : v = - v ↔ v = 0 :=
+by rw [← two_nsmul_eq_zero R M, two_smul, add_eq_zero_iff_eq_neg]
+
+lemma neg_eq_self {v : M} : - v = v ↔ v = 0 :=
+by rw [eq_comm, self_eq_neg R M]
+
+lemma self_ne_neg {v : M} : v ≠ -v ↔ v ≠ 0 :=
+(self_eq_neg R M).not
+
+lemma neg_ne_self {v : M} : -v ≠ v ↔ v ≠ 0 :=
+(neg_eq_self R M).not
 
 end nat
 
@@ -589,15 +591,6 @@ lemma smul_left_injective {x : M} (hx : x ≠ 0) :
 
 end smul_injective
 
-section nat
-
-variables [char_zero R]
-
-lemma ne_neg_of_ne_zero [no_zero_divisors R] {v : R} (hv : v ≠ 0) : v ≠ -v :=
-λ h, hv (eq_zero_of_eq_neg R h)
-
-end nat
-
 end module
 
 section division_ring
diff --git a/src/analysis/normed_space/basic.lean b/src/analysis/normed_space/basic.lean
index f5e4af556b022..f5901240c148a 100644
--- a/src/analysis/normed_space/basic.lean
+++ b/src/analysis/normed_space/basic.lean
@@ -674,7 +674,7 @@ def homeomorph_unit_ball {E : Type*} [semi_normed_group E] [normed_space ℝ E]
 variables (α)
 
 lemma ne_neg_of_mem_sphere [char_zero α] {r : ℝ} (hr : r ≠ 0) (x : sphere (0:E) r) : x ≠ - x :=
-λ h, ne_zero_of_mem_sphere hr x (eq_zero_of_eq_neg α (by { conv_lhs {rw h}, simp }))
+λ h, ne_zero_of_mem_sphere hr x ((self_eq_neg α _).mp (by { conv_lhs {rw h}, simp }))
 
 lemma ne_neg_of_mem_unit_sphere [char_zero α] (x : sphere (0:E) 1) : x ≠ - x :=
 ne_neg_of_mem_sphere α one_ne_zero x
diff --git a/src/measure_theory/integral/bochner.lean b/src/measure_theory/integral/bochner.lean
index 77a7394ccaa22..ca1e12c6ee119 100644
--- a/src/measure_theory/integral/bochner.lean
+++ b/src/measure_theory/integral/bochner.lean
@@ -1331,7 +1331,7 @@ to a left-invariant measure is 0. -/
 lemma integral_zero_of_mul_left_eq_neg [is_mul_left_invariant μ] {f : G → E} {g : G}
   (hf' : ∀ x, f (g * x) = - f x) :
   ∫ x, f x ∂μ = 0 :=
-by { refine eq_zero_of_eq_neg ℝ _, simp_rw [← integral_neg, ← hf', integral_mul_left_eq_self] }
+by simp_rw [← self_eq_neg ℝ E, ← integral_neg, ← hf', integral_mul_left_eq_self]
 
 /-- If some right-translate of a function negates it, then the integral of the function with respect
 to a right-invariant measure is 0. -/
@@ -1339,7 +1339,7 @@ to a right-invariant measure is 0. -/
 lemma integral_zero_of_mul_right_eq_neg [is_mul_right_invariant μ] {f : G → E} {g : G}
   (hf' : ∀ x, f (x * g) = - f x) :
   ∫ x, f x ∂μ = 0 :=
-by { refine eq_zero_of_eq_neg ℝ _, simp_rw [← integral_neg, ← hf', integral_mul_right_eq_self] }
+by simp_rw [← self_eq_neg ℝ E, ← integral_neg, ← hf', integral_mul_right_eq_self]
 
 end group