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

refactor(library/algebra/group): remove unnecessary symm

Browse source
This commit is contained in:
Leonardo de Moura 2015-01-20 16:08:58 -08:00
parent b6750e9d29
commit abc64fbab8
2 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
hott/algebra/group.hlean
View file

@ -427,7 +427,7 @@ section add_group
theorem minus_zero (a : A) : a - 0 = a := (neg_zero⁻¹) ▹ !add_right_id
theorem minus_neg_eq_add (a b : A) : a - (-b) = a + b := !neg_neg⁻¹ ▹ idp
theorem minus_neg_eq_add (a b : A) : a - (-b) = a + b := !neg_neg ▹ idp
theorem neg_minus_eq (a b : A) : -(a - b) = b - a :=
neg_unique

2
library/algebra/group.lean
View file

@ -424,7 +424,7 @@ section add_group
theorem sub_zero (a : A) : a - 0 = a := subst (eq.symm neg_zero) !add_zero
theorem sub_neg_eq_add (a b : A) : a - (-b) = a + b := !neg_neg⁻¹ ▸ rfl
theorem sub_neg_eq_add (a b : A) : a - (-b) = a + b := !neg_neg ▸ rfl
theorem neg_sub (a b : A) : -(a - b) = b - a :=
neg_eq_of_add_eq_zero