Leonardo de Moura
|
52564ecc0f
|
refactor(library/algebra/group_power): open namespaces in the "right" order
|
2015-06-27 14:51:00 -07:00 |
|
Leonardo de Moura
|
ca0aa4eb47
|
feat(library/composition_manager): simplify compositions of the form (mk ... (proj (mk ...)) ...)
closes #666
|
2015-06-27 14:07:32 -07:00 |
|
Leonardo de Moura
|
3215af3926
|
feat(frontends/lean): add '[trans-instance]' attribute
see issue #666
|
2015-06-27 14:07:29 -07:00 |
|
Leonardo de Moura
|
c9f3b766f8
|
refactor(library/algebra/category/constructions): modify proof
It was affected by the new way of handling projections that we will implement
|
2015-06-25 17:48:26 -07:00 |
|
Rob Lewis
|
82950e1c52
|
chore(library/algebra/ordered_field): remove redundant line in calc
|
2015-06-25 17:30:12 -07:00 |
|
Leonardo de Moura
|
018518f0cf
|
refactor(library/algebra/ring): more robust proofs
|
2015-06-22 15:31:03 -07:00 |
|
Leonardo de Moura
|
7ffabeb245
|
refactor(library/algebra/group): avoid abuse of rewrite tactic
The two instances are relying on the fact that (a - b) reduces to (a + -b)
|
2015-06-22 15:11:14 -07:00 |
|
Leonardo de Moura
|
cfafc90cc0
|
refactor(hott,library): make sure files compile even without using "projection macros"
|
2015-06-22 12:22:11 -07:00 |
|
Leonardo de Moura
|
5f293cee9c
|
refactor(library/algebra/ordered_field): improve compilation time
|
2015-06-18 16:12:24 -07:00 |
|
Rob Lewis
|
f7ab2780d4
|
feat(library/algebra): move more theorems from reals to algebra)
|
2015-06-16 11:30:12 -07:00 |
|
Rob Lewis
|
b94d0a948d
|
chore(library/data/real): replace theorems with more general versions from algebra
|
2015-06-16 11:30:12 -07:00 |
|
Rob Lewis
|
b23e23061f
|
feat(library/algebra): finish/move more general theorems from reals to algebra)
|
2015-06-16 11:30:12 -07:00 |
|
Rob Lewis
|
ff0ba6687e
|
feat(library/algebra/ordered_field): move identity about abs to ordered_field
|
2015-06-16 11:30:12 -07:00 |
|
Rob Lewis
|
1f4765e30a
|
feat(library/algebra/ordered_ring): add theorems used for rational upper bounds
|
2015-06-16 11:30:12 -07:00 |
|
Rob Lewis
|
4b38e14586
|
feat(library/algebra/ordered_field): add a couple missing theorems to ordered_field
|
2015-06-16 11:30:12 -07:00 |
|
Jeremy Avigad
|
3b010b8c92
|
feat({library,hott}/algebra/group): add abbreviations e.g. for mul.cancel_left
|
2015-06-15 22:53:11 +10:00 |
|
Leonardo de Moura
|
1bffb89126
|
fix(library/algebra/function): lean was failing to infer that injective is a decidable predicate for finite types with decidable equality
This is an issue reported by Haitao.
|
2015-06-09 15:30:58 -07:00 |
|
Rob Lewis
|
d287b20018
|
chore(library/data/real): move more lemmas to algebra
|
2015-06-09 16:27:55 +10:00 |
|
Rob Lewis
|
7822ba9dee
|
feat(library/algebra): add lemmas to group and ordered group
|
2015-06-09 16:14:21 +10:00 |
|
Jeremy Avigad
|
e59400b58c
|
feat(library/data/int/{div,gcd}): add some theorems, to reduce rationals
|
2015-06-08 22:43:51 +10:00 |
|
Jeremy Avigad
|
df69bb4cfc
|
feat(library/*): add theorems from Haitao on sets and functions, clean up
|
2015-06-04 11:55:25 -07:00 |
|
Jeremy Avigad
|
03952ae12c
|
feat(library/logic/{connectives,identities},library/algebra/function): cleanup and some additions from Haitao Zhang
|
2015-06-04 11:55:25 -07:00 |
|
Jeremy Avigad
|
ffa648a090
|
feat/refactor(library/*): various additions and improvements
|
2015-06-01 12:35:44 +10:00 |
|
Jeremy Avigad
|
b76445df39
|
feat(library/data/{nat,int}/div.lean,*): improve and extend div in nat and int
|
2015-05-30 22:10:21 +10:00 |
|
Jeremy Avigad
|
cc0a620db1
|
feat(library/data/{nat,int}/div.lean): add to and improve div library
|
2015-05-30 22:10:21 +10:00 |
|
Rob Lewis
|
4b67cd1f97
|
feat(library/algebra): update algebraic hierarchy to be more constructive
|
2015-05-29 14:11:50 +10:00 |
|
Rob Lewis
|
eb537daa1c
|
feat(library/algebra): add min/max to ordered algebraic structures
|
2015-05-26 11:45:09 +10:00 |
|
Jeremy Avigad
|
39129f112b
|
refactor(library/*): do various renamings
|
2015-05-25 16:50:42 -07:00 |
|
Jeremy Avigad
|
fdc89cd285
|
refactor(library/algebra/order.lean,library/{data,algebra}/*): use better names for order theorems
|
2015-05-25 16:50:42 -07:00 |
|
Jeremy Avigad
|
7c92161e49
|
refactor(library/data/finset/basic.lean): change order of arguments to induction tactic
|
2015-05-25 16:50:42 -07:00 |
|
Jeremy Avigad
|
8bebd104ff
|
refactor(library/*): remove 'Module:' lines
|
2015-05-23 20:52:23 +10:00 |
|
Jeremy Avigad
|
db7bdce451
|
refactor(logic/funext.lean, algebra/function.lean): delete logic/funext, merge into algebra/function
|
2015-05-23 16:16:36 +10:00 |
|
Jeremy Avigad
|
d33c91d7b9
|
fix({hott,library}/algebra/*): fix names
|
2015-05-23 14:05:06 +10:00 |
|
Leonardo de Moura
|
e1c2340db2
|
fix(frontends/lean): consistent behavior for protected declarations
see https://github.com/leanprover/lean/issues/604#issuecomment-103265608
closes #609
|
2015-05-18 22:35:18 -07:00 |
|
Floris van Doorn
|
2144036cdb
|
feat(hott.circle): prove that the fundamental group of the circle is equal to the integers, as groups
Also many minor fixes at various places
|
2015-05-18 15:59:55 -07:00 |
|
Leonardo de Moura
|
19361f0196
|
feat(library/unifier): do not fire type class resolution as last resort when type contains metavariables
see discussion at #604
|
2015-05-18 15:45:23 -07:00 |
|
Jeremy Avigad
|
566acf4b31
|
feat(library/data/finset/card.lean): add card_Union_of_disjoint and other theorems
|
2015-05-17 19:06:10 +10:00 |
|
Jeremy Avigad
|
6549940c63
|
feat(library/data/finset/bigops.lean): add Union for finsets
|
2015-05-17 17:50:32 +10:00 |
|
Jeremy Avigad
|
9720d84095
|
refactor(library/algebra/group_bigops.lean,library/data/nat/bigops.lean): add ext principle, clean up file
|
2015-05-17 16:00:38 +10:00 |
|
Jeremy Avigad
|
4764f6e8ec
|
refactor(library/algebra/group_bigops.lean,library/data/nat/bigops.lean): simplify naming scheme for bigops
|
2015-05-17 15:24:37 +10:00 |
|
Jeremy Avigad
|
7bde8193fe
|
feat(library/algebra/order): add alternate names for le.antisymm etc.
|
2015-05-17 12:54:36 +10:00 |
|
Jeremy Avigad
|
ff701a9812
|
feat(library/data/nat/bigops.lean): add finite products and sums for nat
|
2015-05-16 22:26:59 +10:00 |
|
Jeremy Avigad
|
eae047bd31
|
refactor,feat(library/{data,algebra}): move bigops to algebra, define sums
|
2015-05-16 18:42:13 +10:00 |
|
Jeremy Avigad
|
87e4f7a951
|
feat(library/algebra/group.lean): add coercions from additive (comm) monoid to (comm) monoid
|
2015-05-16 18:27:49 +10:00 |
|
Jeremy Avigad
|
daf53e4de2
|
fix(library/algebra/order.lean): rename decidable_eq to had_decidable_eq to avoid conflict
|
2015-05-16 17:53:35 +10:00 |
|
Jeremy Avigad
|
8de6a4bb4c
|
feat(library/algebra/group_pow.lean,library/data/nat/power.lean): add generic power operation on monoids and groups
|
2015-05-13 22:19:02 -07:00 |
|
Floris van Doorn
|
0a8f4f6dab
|
feat(function): add unfold hints to function.[h]lean
|
2015-05-07 16:39:03 -07:00 |
|
Leonardo de Moura
|
64cc710ff7
|
refactor(ordered_group): replace 'match' with 'obtain'
|
2015-05-06 10:34:43 -07:00 |
|
Leonardo de Moura
|
cd17618f4a
|
refactor(library): replace 'calc_trans', 'calc_symm', 'calc_refl' and 'calc_subst' commands with attributes '[symm]', '[refl]', '[trans]' and '[subst]'
These attributes are used by the calc command.
They will also be used by tactics such as 'reflexivity', 'symmetry' and
'transitivity'.
See issue #500
|
2015-05-02 15:15:35 -07:00 |
|
Leonardo de Moura
|
3912bc24c8
|
feat(frontends/lean): nicer syntax for 'intros' 'reverts' and 'clears'
|
2015-04-30 11:00:39 -07:00 |
|