From 2e4765482b791ec35bdb56a163d656c8529ddc1e Mon Sep 17 00:00:00 2001 From: Daniel Selsam Date: Fri, 4 Dec 2015 18:55:45 -0800 Subject: [PATCH] fix(algebra/ring): fix names --- library/algebra/ring.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/library/algebra/ring.lean b/library/algebra/ring.lean index 80a157b0a5..431b3fe846 100644 --- a/library/algebra/ring.lean +++ b/library/algebra/ring.lean @@ -196,7 +196,7 @@ section end theorem neg_mul_eq_neg_mul_symm : - a * b = - (a * b) := eq.symm !algebra.neg_mul_eq_neg_mul - theorem neg_mul_eq_mul_neg_symm : a * - b = - (a * b) := eq.symm !algebra.neg_mul_eq_mul_neg + theorem mul_neg_eq_neg_mul_symm : a * - b = - (a * b) := eq.symm !algebra.neg_mul_eq_mul_neg theorem neg_mul_neg : -a * -b = a * b := calc @@ -415,7 +415,7 @@ end unit namespace neg attribute algebra.neg_mul_eq_neg_mul_symm [simp] -attribute algebra.neg_mul_eq_mul_neg_symm [simp] +attribute algebra.mul_neg_eq_neg_mul_symm [simp] end neg namespace distrib