chore(algebra/ring_quot): Provide sub explicitly to ring_quot (#7112

)

This means that using `ring_quot.mk (A - B) = ring_quot.mk A - ring_quot.mk B` is true by definition, even if `A - B = A + -B` is not true by definition.

src/algebra/ring_quot.lean

@@ -47,6 +47,14 @@ theorem rel.neg {R : Type u₁} [ring R] {r : R → R → Prop} ⦃a b : R⦄ (h
   rel r (-a) (-b) :=
 by simp only [neg_eq_neg_one_mul a, neg_eq_neg_one_mul b, rel.mul_right h]
 
+theorem rel.sub_left {R : Type u₁} [ring R] {r : R → R → Prop} ⦃a b c : R⦄ (h : rel r a b) :
+  rel r (a - c) (b - c) :=
+by simp only [sub_eq_add_neg, h.add_left]
+
+theorem rel.sub_right {R : Type u₁} [ring R] {r : R → R → Prop} ⦃a b c : R⦄ (h : rel r b c) :
+  rel r (a - b) (a - c) :=
+by simp only [sub_eq_add_neg, h.neg.add_right]
+
 theorem rel.smul {r : A → A → Prop} (k : S) ⦃a b : A⦄ (h : rel r a b) : rel r (k • a) (k • b) :=
 by simp only [algebra.smul_def, rel.mul_right h]
 
@@ -75,9 +83,10 @@ instance (r : R → R → Prop) : semiring (ring_quot r) :=
   right_distrib := by { rintros ⟨⟩ ⟨⟩ ⟨⟩, exact congr_arg (quot.mk _) (right_distrib _ _ _), }, }
 
 instance {R : Type u₁} [ring R] (r : R → R → Prop) : ring (ring_quot r) :=
-{ neg           := quot.map (λ a, -a)
-    rel.neg,
-  add_left_neg  := by { rintros ⟨⟩, exact congr_arg (quot.mk _) (add_left_neg _), },
+{ neg            := quot.map (λ a, -a) rel.neg,
+  add_left_neg   := by { rintros ⟨⟩, exact congr_arg (quot.mk _) (add_left_neg _), },
+  sub            := quot.map₂ (has_sub.sub) rel.sub_right rel.sub_left,
+  sub_eq_add_neg := by { rintros ⟨⟩ ⟨⟩, exact congr_arg (quot.mk _) (sub_eq_add_neg _ _), },
   .. (ring_quot.semiring r) }
 
 instance {R : Type u₁} [comm_semiring R] (r : R → R → Prop) : comm_semiring (ring_quot r) :=