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

feat(library/algebra/group_power): add times (additive variant of power)

Browse source
This commit is contained in:
François G. Dorais 2015-08-03 12:25:33 -04:00
parent 11b1f416f6
commit 155e22c92c
1 changed files with 1 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
library/algebra/group.lean
View file

@ -584,6 +584,7 @@ section add_comm_group
theorem sub_eq_sub_add_sub (a b c : A) : a - b = c - b + (a - c) := theorem sub_eq_sub_add_sub (a b c : A) : a - b = c - b + (a - c) :=
by rewrite [add_sub, sub_add_cancel] ⬝ !add.comm by rewrite [add_sub, sub_add_cancel] ⬝ !add.comm
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 :=