michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(algebra/ring): fix names

Browse source
This commit is contained in:
Daniel Selsam 2015-12-04 18:55:45 -08:00 committed by Leonardo de Moura
parent 08e0fc796b
commit 2e4765482b
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
library/algebra/ring.lean
View file

@ -196,7 +196,7 @@ section
end end
theorem neg_mul_eq_neg_mul_symm : - a * b = - (a * b) := eq.symm !algebra.neg_mul_eq_neg_mul 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 := theorem neg_mul_neg : -a * -b = a * b :=
calc calc
@ -415,7 +415,7 @@ end unit
namespace neg namespace neg
attribute algebra.neg_mul_eq_neg_mul_symm [simp] 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 end neg
namespace distrib namespace distrib