equal
deleted
inserted
replaced
1 (* |
1 (* |
2 Title: Univariate Polynomials |
2 Title: Univariate Polynomials |
3 Id: $Id$ |
|
4 Author: Clemens Ballarin, started 9 December 1996 |
3 Author: Clemens Ballarin, started 9 December 1996 |
5 Copyright: Clemens Ballarin |
4 Copyright: Clemens Ballarin |
6 *) |
5 *) |
7 |
6 |
8 header {* Univariate Polynomials *} |
7 header {* Univariate Polynomials *} |
386 fix k |
385 fix k |
387 have "coeff (p * monom a 0) k = coeff (a *s p) k" |
386 have "coeff (p * monom a 0) k = coeff (a *s p) k" |
388 proof (cases k) |
387 proof (cases k) |
389 case 0 then show ?thesis by simp ring |
388 case 0 then show ?thesis by simp ring |
390 next |
389 next |
391 case Suc then show ?thesis by (simp add: algebra_simps) ring |
390 case Suc then show ?thesis by simp (ring, simp) |
392 qed |
391 qed |
393 then show "coeff (monom a 0 * p) k = coeff (a *s p) k" by ring |
392 then show "coeff (monom a 0 * p) k = coeff (a *s p) k" by ring |
394 qed |
393 qed |
395 |
394 |
396 ML {* Addsimprocs [ring_simproc] *} |
395 ML {* Addsimprocs [ring_simproc] *} |