Jeremy Avigad
|
9810105a2a
|
refactor(library/data/finste/basic): rename non_empty_of_card_succ to ne_empty_of_card_eq_succ
|
2015-07-11 19:01:44 -04:00 |
|
Jeremy Avigad
|
d443b25dee
|
fix(library/data/{finset,set}/basic: change notation from {[a, b, c]} to '{a, b, c}
|
2015-07-11 19:01:44 -04:00 |
|
Leonardo de Moura
|
9f7c4aac69
|
feat(library): add helper lemmas for equivalent types
|
2015-07-06 12:17:57 -07:00 |
|
Jeremy Avigad
|
7d204fdd91
|
refactor(library/data/finset/card.lean): add useful facts, shorter proof of eq_card_of_eq_subset
|
2015-06-20 21:13:00 -07:00 |
|
Leonardo de Moura
|
ee0d919c6f
|
feat(library/data/finset/card): add eq_of_card_eq_of_subset theorem
|
2015-06-19 20:05:32 -07:00 |
|
Leonardo de Moura
|
2910c780d0
|
feat(library/data/finset/basic): add auxiliary card lemma
|
2015-06-19 20:05:32 -07:00 |
|
Leonardo de Moura
|
4246a64913
|
feat(library/data/finset/basic): add more theorems for finset erase
|
2015-06-19 20:05:32 -07:00 |
|
Leonardo de Moura
|
8fbe22f263
|
refactor(library/data/finset/basic): cleanup proof
|
2015-06-10 18:19:16 -07:00 |
|
Jeremy Avigad
|
3c1f5f4e33
|
feat(library/data/{set,finset}): add more cardinality facts, rename, and add a lemma from Haitao
|
2015-06-10 16:39:17 -07:00 |
|
Jeremy Avigad
|
370860e1b0
|
feat(library/data/fintype,finset): add cardinality for finite types from Haitao Zhang
|
2015-06-05 09:32:00 -07:00 |
|
Jeremy Avigad
|
82142b60f0
|
refactor(library/data/finset/basic.lean): remove finset / finset.finset duplicate
|
2015-06-01 12:35:44 +10: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
|
59c1801921
|
refactor(library/data/{list,set,finset}/basic.lean): make subset reserved notation
|
2015-05-23 12:34:07 +10:00 |
|
Leonardo de Moura
|
3e87f09d78
|
feat(library/tactic/induction_tactic): add support for user-defined recursors that contain parameters that should be synthesized by type class resolution
|
2015-05-19 15:33:46 -07: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 |
|
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
|
783dd61083
|
feat(library/data/finset/basic.lean): add useful calculation rules for quantifiers
|
2015-05-17 17:49:02 +10:00 |
|
Jeremy Avigad
|
81d0d4aa53
|
fix(library/data/{set,finset}/basic.lean: delete \{{ \}}} notation (conflicts with records)
|
2015-05-16 17:53:35 +10:00 |
|
Jeremy Avigad
|
a009cf24e3
|
feat(library/data/finset/{basic,card,comb}.lean: add theorems, including card of an injective image
|
2015-05-11 09:03:57 -07:00 |
|
Jeremy Avigad
|
efbca4c78e
|
feat(library/data/finset/finset.md): add markdown file
|
2015-05-11 09:03:56 -07:00 |
|
Leonardo de Moura
|
3aac370629
|
fix(library/data/finset/basic): type error on the finset.induction proof
|
2015-05-08 11:08:24 -07:00 |
|
Jeremy Avigad
|
4db4c86d37
|
feat(library/data/finset/basic.lean): add lots of theorems, do minor renaming
|
2015-05-08 19:51:37 +10:00 |
|
Leonardo de Moura
|
11f74363e2
|
refactor(library): rename 'intersection' to 'inter' in list and finset, add finset abbreviation at top level
|
2015-05-05 08:53:31 -07:00 |
|
Leonardo de Moura
|
3edf0dffdf
|
feat(library/data/finset): define subset for finsets
|
2015-04-11 15:29:12 -07:00 |
|
Leonardo de Moura
|
dfef4c5daf
|
feat(library/data): define fintype type class
|
2015-04-11 14:55:41 -07:00 |
|
Leonardo de Moura
|
54a2d9750e
|
refactor(library/data): simplify definition of disjoint
|
2015-04-11 14:04:09 -07:00 |
|
Leonardo de Moura
|
dff05557a3
|
feat(library/data/finset): add all combinator theorems
|
2015-04-11 09:28:27 -07:00 |
|
Leonardo de Moura
|
a24c0bf1db
|
feat(library/data/finset): define intersection for finsets
|
2015-04-10 16:45:25 -07:00 |
|
Leonardo de Moura
|
5caa983919
|
feat(library/data/finset): redefine bigop for finset
|
2015-04-10 06:13:32 -07:00 |
|
Leonardo de Moura
|
a223b9b1f7
|
feat(library/data/finset): add bigop for finset + commutative groups
|
2015-04-09 20:00:00 -07:00 |
|
Leonardo de Moura
|
795acc70a6
|
refactor(library/data/finset): move finset to its own directory
|
2015-04-09 19:30:09 -07:00 |
|