Skip to content
This repository was archived by the owner on Jul 24, 2024. It is now read-only.

Commit 3aa5b8a

Browse files
eric-wiesereric-wieser
committed
refactor(algebra/ring/basic): rename lemmas about a*(-b) and (-a)*b (#11925)
This renames: * `(- a) * b = - (a * b)` from `neg_mul_eq_neg_mul_symm` to `neg_mul` * `a * (-b) = - (a * b)` from `mul_neg_eq_neg_mul_symm` to `mul_neg` The new names are much easier to find when compared with `sub_mul`, `mul_sub` etc, and match the existing namespaced names under `units` and `matrix`. This also replaces rewrites by `← neg_mul_eq_neg_mul` with `neg_mul` and rewrites by `← neg_mul_eq_mul_neg` with `mul_neg`. To avoid clashes, the names in the `matrix` namespace are now `protected`. [Zulip](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/mul_neg.2C.20neg_mul/near/233638226)
1 parent 4e17e08 commit 3aa5b8a

59 files changed

Lines changed: 127 additions & 127 deletions

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

‎src/algebra/field/basic.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -79,7 +79,7 @@ calc
7979
1 / (- a) = 1 / ((-1) * a) : by rw neg_eq_neg_one_mul
8080
... = (1 / a) * (1 / (- 1)) : by rw one_div_mul_one_div_rev
8181
... = (1 / a) * (-1) : by rw one_div_neg_one_eq_neg_one
82-
... = - (1 / a) : by rw [mul_neg_eq_neg_mul_symm, mul_one]
82+
... = - (1 / a) : by rw [mul_neg, mul_one]
8383

8484
lemma div_neg_eq_neg_div (a b : K) : b / (- a) = - (b / a) :=
8585
calc

‎src/algebra/geom_sum.lean‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -192,7 +192,7 @@ end
192192

193193
lemma commute.mul_geom_sum₂ [ring α] {x y : α} (h : commute x y) (n : ℕ) :
194194
(x - y) * (geom_sum₂ x y n) = x ^ n - y ^ n :=
195-
by rw [← neg_sub (y ^ n), ← h.mul_neg_geom_sum₂, ← neg_mul_eq_neg_mul_symm, neg_sub]
195+
by rw [← neg_sub (y ^ n), ← h.mul_neg_geom_sum₂, ← neg_mul, neg_sub]
196196

197197
theorem geom_sum₂_mul [comm_ring α] (x y : α) (n : ℕ) :
198198
(geom_sum₂ x y n) * (x - y) = x ^ n - y ^ n :=
@@ -214,7 +214,7 @@ theorem geom_sum_mul_neg [ring α] (x : α) (n : ℕ) :
214214
(geom_sum x n) * (1 - x) = 1 - x ^ n :=
215215
begin
216216
have := congr_arg has_neg.neg (geom_sum_mul x n),
217-
rw [neg_sub, ← mul_neg_eq_neg_mul_symm, neg_sub] at this,
217+
rw [neg_sub, ← mul_neg, neg_sub] at this,
218218
exact this
219219
end
220220

‎src/algebra/group_power/basic.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -396,7 +396,7 @@ by rwa [← add_eq_zero_iff_eq_neg, ← sub_eq_zero, or_comm, ← mul_eq_zero,
396396
← sq_sub_sq a b, sub_eq_zero]
397397

398398
lemma sub_sq (a b : R) : (a - b) ^ 2 = a ^ 2 - 2 * a * b + b ^ 2 :=
399-
by rw [sub_eq_add_neg, add_sq, neg_sq, mul_neg_eq_neg_mul_symm, ← sub_eq_add_neg]
399+
by rw [sub_eq_add_neg, add_sq, neg_sq, mul_neg, ← sub_eq_add_neg]
400400

401401
alias sub_sq ← sub_pow_two
402402

‎src/algebra/order/field.lean‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -207,8 +207,8 @@ lemma div_le_iff_of_neg' (hc : c < 0) : b / c ≤ a ↔ c * a ≤ b :=
207207
by rw [mul_comm, div_le_iff_of_neg hc]
208208

209209
lemma le_div_iff_of_neg (hc : c < 0) : a ≤ b / c ↔ b ≤ a * c :=
210-
by rw [← neg_neg c, mul_neg_eq_neg_mul_symm, div_neg, le_neg,
211-
div_le_iff (neg_pos.2 hc), neg_mul_eq_neg_mul_symm]
210+
by rw [← neg_neg c, mul_neg, div_neg, le_neg,
211+
div_le_iff (neg_pos.2 hc), neg_mul]
212212

213213
lemma le_div_iff_of_neg' (hc : c < 0) : a ≤ b / c ↔ b ≤ c * a :=
214214
by rw [mul_comm, le_div_iff_of_neg hc]

‎src/algebra/order/ring.lean‎

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -900,7 +900,7 @@ protected lemma decidable.mul_le_mul_of_nonpos_left [@decidable_rel α (≤)]
900900
{a b c : α} (h : b ≤ a) (hc : c ≤ 0) : c * a ≤ c * b :=
901901
have -c ≥ 0, from neg_nonneg_of_nonpos hc,
902902
have -c * b ≤ -c * a, from decidable.mul_le_mul_of_nonneg_left h this,
903-
have -(c * b) ≤ -(c * a), by rwa [← neg_mul_eq_neg_mul, ← neg_mul_eq_neg_mul] at this,
903+
have -(c * b) ≤ -(c * a), by rwa [neg_mul, neg_mul] at this,
904904
le_of_neg_le_neg this
905905

906906
lemma mul_le_mul_of_nonpos_left {a b c : α} : b ≤ a → c ≤ 0 → c * a ≤ c * b :=
@@ -911,7 +911,7 @@ protected lemma decidable.mul_le_mul_of_nonpos_right [@decidable_rel α (≤)]
911911
{a b c : α} (h : b ≤ a) (hc : c ≤ 0) : a * c ≤ b * c :=
912912
have -c ≥ 0, from neg_nonneg_of_nonpos hc,
913913
have b * -c ≤ a * -c, from decidable.mul_le_mul_of_nonneg_right h this,
914-
have -(b * c) ≤ -(a * c), by rwa [← neg_mul_eq_mul_neg, ← neg_mul_eq_mul_neg] at this,
914+
have -(b * c) ≤ -(a * c), by rwa [mul_neg, mul_neg] at this,
915915
le_of_neg_le_neg this
916916

917917
lemma mul_le_mul_of_nonpos_right {a b c : α} : b ≤ a → c ≤ 0 → a * c ≤ b * c :=
@@ -929,13 +929,13 @@ by classical; exact decidable.mul_nonneg_of_nonpos_of_nonpos
929929
lemma mul_lt_mul_of_neg_left {a b c : α} (h : b < a) (hc : c < 0) : c * a < c * b :=
930930
have -c > 0, from neg_pos_of_neg hc,
931931
have -c * b < -c * a, from mul_lt_mul_of_pos_left h this,
932-
have -(c * b) < -(c * a), by rwa [← neg_mul_eq_neg_mul, ← neg_mul_eq_neg_mul] at this,
932+
have -(c * b) < -(c * a), by rwa [neg_mul, neg_mul] at this,
933933
lt_of_neg_lt_neg this
934934

935935
lemma mul_lt_mul_of_neg_right {a b c : α} (h : b < a) (hc : c < 0) : a * c < b * c :=
936936
have -c > 0, from neg_pos_of_neg hc,
937937
have b * -c < a * -c, from mul_lt_mul_of_pos_right h this,
938-
have -(b * c) < -(a * c), by rwa [← neg_mul_eq_mul_neg, ← neg_mul_eq_mul_neg] at this,
938+
have -(b * c) < -(a * c), by rwa [mul_neg, mul_neg] at this,
939939
lt_of_neg_lt_neg this
940940

941941
lemma mul_pos_of_neg_of_neg {a b : α} (ha : a < 0) (hb : b < 0) : 0 < a * b :=
@@ -1033,7 +1033,7 @@ begin
10331033
rw [abs_eq (decidable.mul_nonneg (abs_nonneg a) (abs_nonneg b))],
10341034
cases le_total a 0 with ha ha; cases le_total b 0 with hb hb;
10351035
simp only [abs_of_nonpos, abs_of_nonneg, true_or, or_true, eq_self_iff_true,
1036-
neg_mul_eq_neg_mul_symm, mul_neg_eq_neg_mul_symm, neg_neg, *]
1036+
neg_mul, mul_neg, neg_neg, *]
10371037
end
10381038

10391039
/-- `abs` as a `monoid_with_zero_hom`. -/
@@ -1269,7 +1269,7 @@ lemma abs_sub_sq (a b : α) : |a - b| * |a - b| = a * a + b * b - (1 + 1) * a *
12691269
begin
12701270
rw abs_mul_abs_self,
12711271
simp only [mul_add, add_comm, add_left_comm, mul_comm, sub_eq_add_neg,
1272-
mul_one, mul_neg_eq_neg_mul_symm, neg_add_rev, neg_neg],
1272+
mul_one, mul_neg, neg_add_rev, neg_neg],
12731273
end
12741274

12751275
end linear_ordered_comm_ring

‎src/algebra/quaternion.lean‎

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -375,22 +375,22 @@ quaternion_algebra.ext_iff a b
375375
@[simp] lemma mul_re :
376376
(a * b).re = a.re * b.re - a.im_i * b.im_i - a.im_j * b.im_j - a.im_k * b.im_k :=
377377
(quaternion_algebra.has_mul_mul_re a b).trans $
378-
by simp only [one_mul, ← neg_mul_eq_neg_mul, sub_eq_add_neg, neg_neg]
378+
by simp only [one_mul, neg_mul, sub_eq_add_neg, neg_neg]
379379

380380
@[simp] lemma mul_im_i :
381381
(a * b).im_i = a.re * b.im_i + a.im_i * b.re + a.im_j * b.im_k - a.im_k * b.im_j :=
382382
(quaternion_algebra.has_mul_mul_im_i a b).trans $
383-
by simp only [one_mul, ← neg_mul_eq_neg_mul, sub_eq_add_neg, neg_neg]
383+
by simp only [one_mul, neg_mul, sub_eq_add_neg, neg_neg]
384384

385385
@[simp] lemma mul_im_j :
386386
(a * b).im_j = a.re * b.im_j - a.im_i * b.im_k + a.im_j * b.re + a.im_k * b.im_i :=
387387
(quaternion_algebra.has_mul_mul_im_j a b).trans $
388-
by simp only [one_mul, ← neg_mul_eq_neg_mul, sub_eq_add_neg, neg_neg]
388+
by simp only [one_mul, neg_mul, sub_eq_add_neg, neg_neg]
389389

390390
@[simp] lemma mul_im_k :
391391
(a * b).im_k = a.re * b.im_k + a.im_i * b.im_j - a.im_j * b.im_i + a.im_k * b.re :=
392392
(quaternion_algebra.has_mul_mul_im_k a b).trans $
393-
by simp only [one_mul, ← neg_mul_eq_neg_mul, sub_eq_add_neg, neg_neg]
393+
by simp only [one_mul, neg_mul, sub_eq_add_neg, neg_neg]
394394

395395
@[simp, norm_cast] lemma coe_mul : ((x * y : R) : ℍ[R]) = x * y := quaternion_algebra.coe_mul x y
396396

@@ -496,7 +496,7 @@ def norm_sq : ℍ[R] →*₀ R :=
496496
lemma norm_sq_def : norm_sq a = (a * a.conj).re := rfl
497497

498498
lemma norm_sq_def' : norm_sq a = a.1^2 + a.2^2 + a.3^2 + a.4^2 :=
499-
by simp only [norm_sq_def, sq, ← neg_mul_eq_mul_neg, sub_neg_eq_add,
499+
by simp only [norm_sq_def, sq, mul_neg, sub_neg_eq_add,
500500
mul_re, conj_re, conj_im_i, conj_im_j, conj_im_k]
501501

502502
lemma norm_sq_coe : norm_sq (x : ℍ[R]) = x^2 :=

‎src/algebra/quaternion_basis.lean‎

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -81,18 +81,18 @@ attribute [simp] i_mul_i j_mul_j i_mul_j j_mul_i
8181
by rw [←i_mul_j, ←mul_assoc, i_mul_i, smul_mul_assoc, one_mul]
8282

8383
@[simp] lemma k_mul_i : q.k * q.i = -c₁ • q.j :=
84-
by rw [←i_mul_j, mul_assoc, j_mul_i, mul_neg_eq_neg_mul_symm, i_mul_k, neg_smul]
84+
by rw [←i_mul_j, mul_assoc, j_mul_i, mul_neg, i_mul_k, neg_smul]
8585

8686
@[simp] lemma k_mul_j : q.k * q.j = c₂ • q.i :=
8787
by rw [←i_mul_j, mul_assoc, j_mul_j, mul_smul_comm, mul_one]
8888

8989
@[simp] lemma j_mul_k : q.j * q.k = -c₂ • q.i :=
90-
by rw [←i_mul_j, ←mul_assoc, j_mul_i, neg_mul_eq_neg_mul_symm, k_mul_j, neg_smul]
90+
by rw [←i_mul_j, ←mul_assoc, j_mul_i, neg_mul, k_mul_j, neg_smul]
9191

9292
@[simp] lemma k_mul_k : q.k * q.k = -((c₁ * c₂) • 1) :=
9393
by rw [←i_mul_j, mul_assoc, ←mul_assoc q.j _ _, j_mul_i, ←i_mul_j,
94-
←mul_assoc, mul_neg_eq_neg_mul_symm, ←mul_assoc, i_mul_i, smul_mul_assoc, one_mul,
95-
neg_mul_eq_neg_mul_symm, smul_mul_assoc, j_mul_j, smul_smul]
94+
←mul_assoc, mul_neg, ←mul_assoc, i_mul_i, smul_mul_assoc, one_mul,
95+
neg_mul, smul_mul_assoc, j_mul_j, smul_smul]
9696

9797
/-- Intermediate result used to define `quaternion_algebra.basis.lift_hom`. -/
9898
def lift (x : ℍ[R,c₁,c₂]) : A :=
@@ -109,7 +109,7 @@ begin
109109
simp only [add_mul, mul_add, smul_mul_assoc, mul_smul_comm, one_mul, mul_one,
110110
←algebra.smul_def, smul_add, smul_smul],
111111
simp only [i_mul_i, j_mul_j, i_mul_j, j_mul_i, i_mul_k, k_mul_i, k_mul_j, j_mul_k, k_mul_k],
112-
simp only [smul_smul, smul_neg, sub_eq_add_neg, add_smul, ←add_assoc, mul_neg_eq_neg_mul_symm,
112+
simp only [smul_smul, smul_neg, sub_eq_add_neg, add_smul, ←add_assoc, mul_neg,
113113
neg_smul],
114114
simp only [mul_right_comm _ _ (c₁ * c₂), mul_comm _ (c₁ * c₂)],
115115
simp only [mul_comm _ c₁, mul_right_comm _ _ c₁],

‎src/algebra/ring/basic.lean‎

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -716,10 +716,10 @@ lemma neg_mul_eq_mul_neg (a b : α) : -(a * b) = a * -b :=
716716
neg_eq_of_add_eq_zero
717717
begin rw [← left_distrib, add_right_neg, mul_zero] end
718718

719-
@[simp] lemma neg_mul_eq_neg_mul_symm (a b : α) : - a * b = - (a * b) :=
719+
@[simp] lemma neg_mul (a b : α) : - a * b = - (a * b) :=
720720
eq.symm (neg_mul_eq_neg_mul a b)
721721

722-
@[simp] lemma mul_neg_eq_neg_mul_symm (a b : α) : a * - b = - (a * b) :=
722+
@[simp] lemma mul_neg (a b : α) : a * - b = - (a * b) :=
723723
eq.symm (neg_mul_eq_mul_neg a b)
724724

725725
lemma neg_mul_neg (a b : α) : -a * -b = a * b :=
@@ -791,7 +791,7 @@ units.ext $ neg_neg _
791791
/-- Multiplication of elements of a ring's unit group commutes with mapping the first
792792
argument to its additive inverse. -/
793793
@[simp] protected theorem neg_mul (u₁ u₂ : αˣ) : -u₁ * u₂ = -(u₁ * u₂) :=
794-
units.ext $ neg_mul_eq_neg_mul_symm _ _
794+
units.ext $ neg_mul _ _
795795

796796
/-- Multiplication of elements of a ring's unit group commutes with mapping the second argument
797797
to its additive inverse. -/
@@ -929,7 +929,7 @@ lemma odd.neg {a : α} (hp : odd a) : odd (-a) :=
929929
begin
930930
obtain ⟨k, hk⟩ := hp,
931931
use -(k + 1),
932-
rw [mul_neg_eq_neg_mul_symm, mul_add, neg_add, add_assoc, two_mul (1 : α), neg_add,
932+
rw [mul_neg, mul_add, neg_add, add_assoc, two_mul (1 : α), neg_add,
933933
neg_add_cancel_right, ←neg_add, hk],
934934
end
935935

@@ -1137,13 +1137,13 @@ by simp only [semiconj_by, left_distrib, right_distrib, ha.eq, hb.eq]
11371137
variables [ring R] {a b x y x' y' : R}
11381138

11391139
lemma neg_right (h : semiconj_by a x y) : semiconj_by a (-x) (-y) :=
1140-
by simp only [semiconj_by, h.eq, neg_mul_eq_neg_mul_symm, mul_neg_eq_neg_mul_symm]
1140+
by simp only [semiconj_by, h.eq, neg_mul, mul_neg]
11411141

11421142
@[simp] lemma neg_right_iff : semiconj_by a (-x) (-y) ↔ semiconj_by a x y :=
11431143
⟨λ h, neg_neg x ▸ neg_neg y ▸ h.neg_right, semiconj_by.neg_right⟩
11441144

11451145
lemma neg_left (h : semiconj_by a x y) : semiconj_by (-a) x y :=
1146-
by simp only [semiconj_by, h.eq, neg_mul_eq_neg_mul_symm, mul_neg_eq_neg_mul_symm]
1146+
by simp only [semiconj_by, h.eq, neg_mul, mul_neg]
11471147

11481148
@[simp] lemma neg_left_iff : semiconj_by (-a) x y ↔ semiconj_by a x y :=
11491149
⟨λ h, neg_neg a ▸ h.neg_left, semiconj_by.neg_left⟩

‎src/algebra/star/chsh.lean‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -131,7 +131,7 @@ begin
131131
simp only [mul_comm _ (2 : R), mul_comm _ (4 : R),
132132
mul_left_comm _ (2 : R), mul_left_comm _ (4 : R)],
133133
abel,
134-
simp only [neg_mul_eq_neg_mul_symm, mul_one, int.cast_bit0, one_mul, int.cast_one,
134+
simp only [neg_mul, mul_one, int.cast_bit0, one_mul, int.cast_one,
135135
zsmul_eq_mul, int.cast_neg],
136136
simp only [←mul_assoc, ←add_assoc],
137137
norm_num, },
@@ -217,7 +217,7 @@ begin
217217
abel,
218218
-- all terms coincide, but the last one. Simplify all other terms
219219
simp only [M],
220-
simp only [neg_mul_eq_neg_mul_symm, int.cast_bit0, one_mul, mul_inv_cancel_of_invertible,
220+
simp only [neg_mul, int.cast_bit0, one_mul, mul_inv_cancel_of_invertible,
221221
int.cast_one, one_smul, int.cast_neg, add_right_inj, neg_smul, ← add_smul],
222222
-- just look at the coefficients now:
223223
congr,

‎src/algebraic_geometry/structure_sheaf.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -190,7 +190,7 @@ def sections_subring (U : (opens (prime_spectrum.Top R))ᵒᵖ) :
190190
{ exact nm, },
191191
{ simp only [ring_hom.map_neg, pi.neg_apply],
192192
erw [←w],
193-
simp only [neg_mul_eq_neg_mul_symm], }
193+
simp only [neg_mul], }
194194
end,
195195
mul_mem' :=
196196
begin

0 commit comments

Comments
 (0)