| Wed, 18 Feb 2009 09:47:58 -0800 |
huffman |
move polynomial order stuff from Fundamental_Theorem_Algebra to Polynomial
|
file |
diff |
annotate
|
| Fri, 13 Feb 2009 14:12:00 -0800 |
huffman |
add class cancel_comm_monoid_add
|
file |
diff |
annotate
|
| Wed, 11 Feb 2009 11:22:42 -0800 |
huffman |
ordered_idom instance for polynomials
|
file |
diff |
annotate
|
| Wed, 28 Jan 2009 16:57:12 +0100 |
nipkow |
merged - resolving conflics
|
file |
diff |
annotate
|
| Wed, 28 Jan 2009 16:29:16 +0100 |
nipkow |
Replaced group_ and ring_simps by algebra_simps;
|
file |
diff |
annotate
|
| Wed, 28 Jan 2009 06:03:46 -0800 |
huffman |
merged
|
file |
diff |
annotate
|
| Wed, 21 Jan 2009 21:01:15 -0800 |
huffman |
add lemmas about div/mod with multiplication
|
file |
diff |
annotate
|
| Wed, 21 Jan 2009 20:20:56 -0800 |
huffman |
add lemmas about smult
|
file |
diff |
annotate
|
| Wed, 28 Jan 2009 11:03:16 +0100 |
haftmann |
Plain, Main form meeting points in import hierarchy
|
file |
diff |
annotate
|
| Thu, 15 Jan 2009 12:43:41 -0800 |
huffman |
more instance declarations for poly
|
file |
diff |
annotate
|
| Thu, 15 Jan 2009 12:43:12 -0800 |
huffman |
add lemmas about degree
|
file |
diff |
annotate
|
| Thu, 15 Jan 2009 09:17:15 -0800 |
huffman |
rename divmod_poly to pdivmod
|
file |
diff |
annotate
|
| Tue, 13 Jan 2009 15:33:30 -0800 |
huffman |
declare pCons_0_0 [code post]
|
file |
diff |
annotate
|
| Tue, 13 Jan 2009 13:48:21 -0800 |
huffman |
code generation for polynomials
|
file |
diff |
annotate
|
| Tue, 13 Jan 2009 10:18:23 -0800 |
huffman |
declare more definitions [code del]
|
file |
diff |
annotate
|
| Tue, 13 Jan 2009 08:58:56 -0800 |
huffman |
define polynomial multiplication using poly_rec
|
file |
diff |
annotate
|
| Tue, 13 Jan 2009 08:19:14 -0800 |
huffman |
declare smult rules [simp]
|
file |
diff |
annotate
|
| Tue, 13 Jan 2009 07:40:05 -0800 |
huffman |
simplify proof of coeff_mult_degree_sum
|
file |
diff |
annotate
|
| Mon, 12 Jan 2009 22:16:35 -0800 |
huffman |
add lemmas poly_power, poly_roots_finite
|
file |
diff |
annotate
|
| Mon, 12 Jan 2009 12:09:54 -0800 |
huffman |
new lemmas about synthetic_div; declare degree_pCons_eq_if [simp]
|
file |
diff |
annotate
|
| Mon, 12 Jan 2009 10:09:23 -0800 |
huffman |
correctness and uniqueness of synthetic division
|
file |
diff |
annotate
|
| Mon, 12 Jan 2009 09:35:15 -0800 |
huffman |
add synthetic division algorithm for polynomials
|
file |
diff |
annotate
|
| Mon, 12 Jan 2009 09:04:25 -0800 |
huffman |
add list-style syntax for pCons
|
file |
diff |
annotate
|
| Mon, 12 Jan 2009 08:46:07 -0800 |
huffman |
add recursion combinator poly_rec; define poly function using poly_rec
|
file |
diff |
annotate
|
| Mon, 12 Jan 2009 08:15:07 -0800 |
huffman |
add lemmas degree_{add,diff}_less
|
file |
diff |
annotate
|
| Sun, 11 Jan 2009 12:05:50 -0800 |
huffman |
new theory of polynomials
|
file |
diff |
annotate
|