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

refactor(library/algebra/group): rename neg_add_distrib to neg_add, etc.

Browse source
This commit is contained in:
Jeremy Avigad 2015-01-26 11:42:13 -05:00
parent ba15da8d83
commit 85ef7c5151
3 changed files with 8 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
library/algebra/group.lean
View file

@ -341,7 +341,7 @@ section add_group
... = a + 0 : add.right_inv ... = a + 0 : add.right_inv
... = a : add_zero ... = a : add_zero
theorem neg_add (a b : A) : -(a + b) = -b + -a := theorem neg_add_rev (a b : A) : -(a + b) = -b + -a :=
neg_eq_of_add_eq_zero neg_eq_of_add_eq_zero
(calc (calc
a + b + (-b + -a) = a + (b + (-b + -a)) : add.assoc a + b + (-b + -a) = a + (b + (-b + -a)) : add.assoc
@ -437,7 +437,7 @@ section add_group
theorem sub_add_eq_sub_sub_swap (a b c : A) : a - (b + c) = a - c - b := theorem sub_add_eq_sub_sub_swap (a b c : A) : a - (b + c) = a - c - b :=
calc calc
a - (b + c) = a + (-c - b) : neg_add a - (b + c) = a + (-c - b) : neg_add_rev
... = a - c - b : !add.assoc⁻¹ ... = a - c - b : !add.assoc⁻¹
theorem sub_eq_iff_eq_add (a b c : A) : a - b = c ↔ a = c + b := theorem sub_eq_iff_eq_add (a b c : A) : a - b = c ↔ a = c + b :=
@ -466,14 +466,14 @@ include s
theorem neg_add_eq_sub (a b : A) : -a + b = b - a := !add.comm theorem neg_add_eq_sub (a b : A) : -a + b = b - a := !add.comm
theorem neg_add_distrib (a b : A) : -(a + b) = -a + -b := add.comm (-b) (-a) ▸ neg_add a b theorem neg_add (a b : A) : -(a + b) = -a + -b := add.comm (-b) (-a) ▸ neg_add_rev a b
theorem sub_add_eq_add_sub (a b c : A) : a - b + c = a + c - b := !add.right_comm theorem sub_add_eq_add_sub (a b c : A) : a - b + c = a + c - b := !add.right_comm
theorem sub_sub (a b c : A) : a - b - c = a - (b + c) := theorem sub_sub (a b c : A) : a - b - c = a - (b + c) :=
calc calc
a - b - c = a + (-b + -c) : add.assoc a - b - c = a + (-b + -c) : add.assoc
... = a + -(b + c) : {(neg_add_distrib b c)⁻¹} ... = a + -(b + c) : {(neg_add b c)⁻¹}
... = a - (b + c) : rfl ... = a - (b + c) : rfl
theorem add_sub_add_left_eq_sub (a b c : A) : (c + a) - (c + b) = a - b := theorem add_sub_add_left_eq_sub (a b c : A) : (c + a) - (c + b) = a - b :=

4
library/algebra/ordered_group.lean
View file

@ -525,11 +525,11 @@ section
or.elim (le.total 0 (a + b)) or.elim (le.total 0 (a + b))
(assume H2 : 0 ≤ a + b, aux2 H2) (assume H2 : 0 ≤ a + b, aux2 H2)
(assume H2 : a + b ≤ 0, (assume H2 : a + b ≤ 0,
have H3 : -a + -b = -(a + b), from !neg_add_distrib⁻¹, have H3 : -a + -b = -(a + b), from !neg_add⁻¹,
have H4 : -(a + b) ≥ 0, from iff.mp' !neg_nonneg_iff_nonpos H2, have H4 : -(a + b) ≥ 0, from iff.mp' !neg_nonneg_iff_nonpos H2,
calc calc
|a + b| = |-(a + b)| : abs_neg |a + b| = |-(a + b)| : abs_neg
... = |-a + -b| : neg_add_distrib ... = |-a + -b| : neg_add
... ≤ |-a| + |-b| : aux2 (H3⁻¹ ▸ H4) ... ≤ |-a| + |-b| : aux2 (H3⁻¹ ▸ H4)
... = |a| + |-b| : abs_neg ... = |a| + |-b| : abs_neg
... = |a| + |b| : abs_neg) ... = |a| + |b| : abs_neg)

4
library/data/int/basic.lean
View file

@ -640,7 +640,7 @@ section port_algebra
theorem add.right_inv : ∀a : ℤ, a + -a = 0 := algebra.add.right_inv theorem add.right_inv : ∀a : ℤ, a + -a = 0 := algebra.add.right_inv
theorem add_neg_cancel_left : ∀a b : ℤ, a + (-a + b) = b := algebra.add_neg_cancel_left theorem add_neg_cancel_left : ∀a b : ℤ, a + (-a + b) = b := algebra.add_neg_cancel_left
theorem add_neg_cancel_right : ∀a b : ℤ, a + b + -b = a := algebra.add_neg_cancel_right theorem add_neg_cancel_right : ∀a b : ℤ, a + b + -b = a := algebra.add_neg_cancel_right
theorem neg_add : ∀a b : ℤ, -(a + b) = -b + -a := algebra.neg_add theorem neg_add_rev : ∀a b : ℤ, -(a + b) = -b + -a := algebra.neg_add_rev
theorem eq_add_neg_of_add_eq : ∀{a b c : ℤ}, a + b = c → a = c + -b := theorem eq_add_neg_of_add_eq : ∀{a b c : ℤ}, a + b = c → a = c + -b :=
@algebra.eq_add_neg_of_add_eq _ _ @algebra.eq_add_neg_of_add_eq _ _
theorem eq_neg_add_of_add_eq : ∀{a b c : ℤ}, a + b = c → b = -a + c := theorem eq_neg_add_of_add_eq : ∀{a b c : ℤ}, a + b = c → b = -a + c :=
@ -681,7 +681,7 @@ section port_algebra
@algebra.eq_iff_eq_of_sub_eq_sub _ _ @algebra.eq_iff_eq_of_sub_eq_sub _ _
theorem sub_add_eq_sub_sub : ∀a b c : ℤ, a - (b + c) = a - b - c := algebra.sub_add_eq_sub_sub theorem sub_add_eq_sub_sub : ∀a b c : ℤ, a - (b + c) = a - b - c := algebra.sub_add_eq_sub_sub
theorem neg_add_eq_sub : ∀a b : ℤ, -a + b = b - a := algebra.neg_add_eq_sub theorem neg_add_eq_sub : ∀a b : ℤ, -a + b = b - a := algebra.neg_add_eq_sub
theorem neg_add_distrib : ∀a b : ℤ, -(a + b) = -a + -b := algebra.neg_add_distrib theorem neg_add : ∀a b : ℤ, -(a + b) = -a + -b := algebra.neg_add
theorem sub_add_eq_add_sub : ∀a b c : ℤ, a - b + c = a + c - b := algebra.sub_add_eq_add_sub theorem sub_add_eq_add_sub : ∀a b c : ℤ, a - b + c = a + c - b := algebra.sub_add_eq_add_sub
theorem sub_sub_ : ∀a b c : ℤ, a - b - c = a - (b + c) := algebra.sub_sub theorem sub_sub_ : ∀a b c : ℤ, a - b - c = a - (b + c) := algebra.sub_sub
theorem add_sub_add_left_eq_sub : ∀a b c : ℤ, (c + a) - (c + b) = a - b := theorem add_sub_add_left_eq_sub : ∀a b c : ℤ, (c + a) - (c + b) = a - b :=