refactor(algebra/ring/basic): replace neg_zero' by neg_zero_class…

… instance (#16686)

Eliminate the separate `neg_zero'` lemma for the combination of `mul_zero_class` with `has_distrib_neg` by adding a `neg_zero_class` instance for that case.

src/algebra/ring/basic.lean

@@ -542,9 +542,11 @@ end mul_one_class
 section mul_zero_class
 variables [mul_zero_class α] [has_distrib_neg α]
 
-/-- Prefer `neg_zero` if `subtraction_monoid` is available. -/
-@[simp] lemma neg_zero' : (-0 : α) = 0 :=
-by rw [←zero_mul (0 : α), ←neg_mul, mul_zero, mul_zero]
+@[priority 100]
+instance mul_zero_class.neg_zero_class : neg_zero_class α :=
+{ neg_zero := by rw [←zero_mul (0 : α), ←neg_mul, mul_zero, mul_zero],
+  ..mul_zero_class.to_has_zero α,
+  ..has_distrib_neg.to_has_involutive_neg α }
 
 end mul_zero_class
 

src/analysis/special_functions/pow.lean

@@ -651,7 +651,7 @@ le_iff_le_iff_lt_iff_lt.2 $ rpow_lt_rpow_iff hy hx hz
 lemma le_rpow_inv_iff_of_neg (hx : 0 < x) (hy : 0 < y) (hz : z < 0) :
   x ≤ y ^ z⁻¹ ↔ y ≤ x ^ z :=
 begin
-  have hz' : 0 < -z := by rwa [lt_neg, neg_zero'],
+  have hz' : 0 < -z := by rwa [lt_neg, neg_zero],
   have hxz : 0 < x ^ (-z) := real.rpow_pos_of_pos hx _,
   have hyz : 0 < y ^ z⁻¹ := real.rpow_pos_of_pos hy _,
   rw [←real.rpow_le_rpow_iff hx.le hyz.le hz', ←real.rpow_mul hy.le],
@@ -663,7 +663,7 @@ end
 lemma lt_rpow_inv_iff_of_neg (hx : 0 < x) (hy : 0 < y) (hz : z < 0) :
   x < y ^ z⁻¹ ↔ y < x ^ z :=
 begin
-  have hz' : 0 < -z := by rwa [lt_neg, neg_zero'],
+  have hz' : 0 < -z := by rwa [lt_neg, neg_zero],
   have hxz : 0 < x ^ (-z) := real.rpow_pos_of_pos hx _,
   have hyz : 0 < y ^ z⁻¹ := real.rpow_pos_of_pos hy _,
   rw [←real.rpow_lt_rpow_iff hx.le hyz.le hz', ←real.rpow_mul hy.le],

src/data/polynomial/laurent.lean

@@ -355,7 +355,7 @@ lemma reduce_to_polynomial_of_mul_T (f : R[T;T⁻¹]) {Q : R[T;T⁻¹] → Prop}
 begin
   induction f using laurent_polynomial.induction_on_mul_T with f n,
   induction n with n hn,
-  { simpa only [int.coe_nat_zero, neg_zero', T_zero, mul_one] using Qf _ },
+  { simpa only [int.coe_nat_zero, neg_zero, T_zero, mul_one] using Qf _ },
   { convert QT _ _,
     simpa using hn }
 end

src/data/sign.lean

@@ -283,7 +283,7 @@ lemma sign_mul (x y : α) : sign (x * y) = sign x * sign y :=
 begin
   rcases lt_trichotomy x 0 with hx | hx | hx; rcases lt_trichotomy y 0 with hy | hy | hy;
     simp only [sign_zero, mul_zero, zero_mul, sign_pos, sign_neg, hx, hy, mul_one, neg_one_mul,
-               neg_neg, one_mul, mul_pos_of_neg_of_neg, mul_neg_of_neg_of_pos, neg_zero',
+               neg_neg, one_mul, mul_pos_of_neg_of_neg, mul_neg_of_neg_of_pos, neg_zero,
                mul_neg_of_pos_of_neg, mul_pos]
 end
 

src/linear_algebra/symplectic_group.lean

@@ -47,7 +47,7 @@ variables [fintype l]
 lemma J_squared : (J l R) ⬝ (J l R) = -1 :=
 begin
   rw [J, from_blocks_multiply],
-  simp only [matrix.zero_mul, matrix.neg_mul, zero_add, neg_zero', matrix.one_mul, add_zero],
+  simp only [matrix.zero_mul, matrix.neg_mul, zero_add, neg_zero, matrix.one_mul, add_zero],
   rw [← neg_zero, ← matrix.from_blocks_neg, ← from_blocks_one],
 end
 

src/probability/moments.lean

@@ -59,7 +59,7 @@ by simp only [moment, hp, zero_pow', ne.def, not_false_iff, pi.zero_apply, integ
 
 @[simp] lemma central_moment_zero (hp : p ≠ 0) : central_moment 0 p μ = 0 :=
 by simp only [central_moment, hp, pi.zero_apply, integral_const, algebra.id.smul_eq_mul,
-  mul_zero, zero_sub, pi.pow_apply, pi.neg_apply, neg_zero', zero_pow', ne.def, not_false_iff]
+  mul_zero, zero_sub, pi.pow_apply, pi.neg_apply, neg_zero, zero_pow', ne.def, not_false_iff]
 
 lemma central_moment_one' [is_finite_measure μ] (h_int : integrable X μ) :
   central_moment X 1 μ = (1 - (μ set.univ).to_real) * μ[X] :=
@@ -307,7 +307,7 @@ lemma measure_ge_le_exp_mul_mgf [is_finite_measure μ] (ε : ℝ) (ht : 0 ≤ t)
 begin
   cases ht.eq_or_lt with ht_zero_eq ht_pos,
   { rw ht_zero_eq.symm,
-    simp only [neg_zero', zero_mul, exp_zero, mgf_zero', one_mul],
+    simp only [neg_zero, zero_mul, exp_zero, mgf_zero', one_mul],
     rw ennreal.to_real_le_to_real (measure_ne_top μ _) (measure_ne_top μ _),
     exact measure_mono (set.subset_univ _), },
   calc (μ {ω | ε ≤ X ω}).to_real