Jeremy Avigad
|
d9098ff4e5
|
fix(library/theories/number_theory/bezout): make duplicate proof of prime -> irreducible an example
|
2015-07-07 21:05:48 -07:00 |
|
Leonardo de Moura
|
db1fae0461
|
feat(library/theories/number_theory/primes): cleanup proofs
|
2015-07-05 08:21:16 -07:00 |
|
Leonardo de Moura
|
d1b5a6be54
|
feat(library/theories/number_theory/primes): add Haitao's divisor_of_prime_pow lemma
|
2015-07-04 13:27:10 -07:00 |
|
Leonardo de Moura
|
f4f77e7f0b
|
feat(library): move data/nat/primes to theories/number_theory
|
2015-07-04 09:49:14 -07:00 |
|
Jeremy Avigad
|
a776e13c3b
|
feat(library/theories/number_theory/bezout): for nat, irreducible implies prime
|
2015-07-04 22:56:55 +10:00 |
|
Jeremy Avigad
|
54128eb45f
|
feat(library/theories/number_theory/bezout): add Bezout's theorem, adapted from William Peterson's project
|
2015-06-27 19:13:36 +10:00 |
|