From c8771b6bbec0fb5a427bd58c52a305a1015c15a8 Mon Sep 17 00:00:00 2001 From: Bryan Gin-ge Chen Date: Sat, 12 Sep 2020 16:34:13 +0000 Subject: [PATCH] fix(algebra/ring/basic): delete mul_self_sub_mul_self_eq (#4119) It's redundant with `mul_self_sub_mul_self`. Also renamed `mul_self_sub_one_eq` to `mul_self_sub_one`. --- src/algebra/ring/basic.lean | 9 +++------ 1 file changed, 3 insertions(+), 6 deletions(-) diff --git a/src/algebra/ring/basic.lean b/src/algebra/ring/basic.lean index f8708c2b2eee7..85d4b86509125 100644 --- a/src/algebra/ring/basic.lean +++ b/src/algebra/ring/basic.lean @@ -582,12 +582,6 @@ protected def function.surjective.comm_ring [has_zero β] [has_one β] [has_add local attribute [simp] add_assoc add_comm add_left_comm mul_comm -lemma mul_self_sub_mul_self_eq (a b : α) : a * a - b * b = (a + b) * (a - b) := -by simp [right_distrib, left_distrib, sub_eq_add_neg] - -lemma mul_self_sub_one_eq (a : α) : a * a - 1 = (a + 1) * (a - 1) := -by rw [← mul_self_sub_mul_self_eq, mul_one] - theorem dvd_neg_of_dvd (h : a ∣ b) : (a ∣ -b) := dvd.elim h (assume c, assume : b = a * c, @@ -625,6 +619,9 @@ theorem two_dvd_bit1 : 2 ∣ bit1 a ↔ (2 : α) ∣ 1 := (dvd_add_iff_right (@t theorem mul_self_sub_mul_self (a b : α) : a * a - b * b = (a + b) * (a - b) := by rw [add_mul, mul_sub, mul_sub, mul_comm a b, sub_add_sub_cancel] +lemma mul_self_sub_one (a : α) : a * a - 1 = (a + 1) * (a - 1) := +by rw [← mul_self_sub_mul_self, mul_one] + /-- An element a of a commutative ring divides the additive inverse of an element b iff a divides b. -/ @[simp] lemma dvd_neg (a b : α) : (a ∣ -b) ↔ (a ∣ b) :=