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

feat({library,hott}/algebra/group): add abbreviations e.g. for mul.cancel_left

Browse source
This commit is contained in:
Jeremy Avigad 2015-06-15 21:16:30 +10:00
parent a4a8253f50
commit 3b010b8c92
2 changed files with 16 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
hott/algebra/group.hlean
View file

@ -74,6 +74,8 @@ theorem mul.left_cancel [s : left_cancel_semigroup A] {a b c : A} :
a * b = a * c → b = c :=
!left_cancel_semigroup.mul_left_cancel
abbreviation eq_of_mul_eq_mul_left' := @mul.left_cancel
structure right_cancel_semigroup [class] (A : Type) extends semigroup A :=
(mul_right_cancel : ∀a b c, mul a b = mul c b → a = c)
@ -81,6 +83,8 @@ theorem mul.right_cancel [s : right_cancel_semigroup A] {a b c : A} :
a * b = c * b → a = c :=
!right_cancel_semigroup.mul_right_cancel
abbreviation eq_of_mul_eq_mul_right' := @mul.right_cancel
/- additive semigroup -/
structure add_semigroup [class] (A : Type) extends has_add A :=
@ -112,6 +116,8 @@ theorem add.left_cancel [s : add_left_cancel_semigroup A] {a b c : A} :
a + b = a + c → b = c :=
!add_left_cancel_semigroup.add_left_cancel
abbreviation eq_of_add_eq_add_left := @add.left_cancel
structure add_right_cancel_semigroup [class] (A : Type) extends add_semigroup A :=
(add_right_cancel : ∀a b c, add a b = add c b → a = c)
@ -119,6 +125,8 @@ theorem add.right_cancel [s : add_right_cancel_semigroup A] {a b c : A} :
a + b = c + b → a = c :=
!add_right_cancel_semigroup.add_right_cancel
abbreviation eq_of_add_eq_add_right := @add.right_cancel
/- monoid -/
structure monoid [class] (A : Type) extends semigroup A, has_one A :=

8
library/algebra/group.lean
View file

@ -70,6 +70,8 @@ theorem mul.left_cancel [s : left_cancel_semigroup A] {a b c : A} :
a * b = a * c → b = c :=
!left_cancel_semigroup.mul_left_cancel
abbreviation eq_of_mul_eq_mul_left' := @mul.left_cancel
structure right_cancel_semigroup [class] (A : Type) extends semigroup A :=
(mul_right_cancel : ∀a b c, mul a b = mul c b → a = c)
@ -77,6 +79,8 @@ theorem mul.right_cancel [s : right_cancel_semigroup A] {a b c : A} :
a * b = c * b → a = c :=
!right_cancel_semigroup.mul_right_cancel
abbreviation eq_of_mul_eq_mul_right' := @mul.right_cancel
/- additive semigroup -/
structure add_semigroup [class] (A : Type) extends has_add A :=
@ -105,6 +109,8 @@ theorem add.left_cancel [s : add_left_cancel_semigroup A] {a b c : A} :
a + b = a + c → b = c :=
!add_left_cancel_semigroup.add_left_cancel
abbreviation eq_of_add_eq_add_left := @add.left_cancel
structure add_right_cancel_semigroup [class] (A : Type) extends add_semigroup A :=
(add_right_cancel : ∀a b c, add a b = add c b → a = c)
@ -112,6 +118,8 @@ theorem add.right_cancel [s : add_right_cancel_semigroup A] {a b c : A} :
a + b = c + b → a = c :=
!add_right_cancel_semigroup.add_right_cancel
abbreviation eq_of_add_eq_add_right := @add.right_cancel
/- monoid -/
structure monoid [class] (A : Type) extends semigroup A, has_one A :=