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

feat(library/algebra/group): add theorem to comm group

Browse source
This commit is contained in:
Rob Lewis 2015-07-31 10:54:06 -04:00 committed by Leonardo de Moura
parent 0c65468db3
commit 1693932c9f
1 changed files with 4 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
library/algebra/group.lean
View file

@ -558,6 +558,10 @@ section add_comm_group
theorem add_eq_of_eq_sub' {a b c : A} (H : b = c - a) : a + b = c := theorem add_eq_of_eq_sub' {a b c : A} (H : b = c - a) : a + b = c :=
!add.comm ▸ add_eq_of_eq_sub H !add.comm ▸ add_eq_of_eq_sub H
theorem sub_sub_self (a b : A) : a - (a - b) = b :=
by rewrite [sub_eq_add_neg, neg_sub, add.comm, sub_add_cancel]
end add_comm_group end add_comm_group
definition group_of_add_group (A : Type) [G : add_group A] : group A := definition group_of_add_group (A : Type) [G : add_group A] : group A :=