[Isarmathlib-devel] Re: Polynomial ring

[Sanghyeon Seo]

Some progress: the result of adding two polynomials is a polynomial.
Not quite that...

1. Proved that A <= A Un B.
2. Proved that if n > degree(X), coefficient(X,n) = 0.
3. When A+B=C for polynomials A, B, C, if we let d = degree(A) Un degree(B),
then using 1, if n > d then n > degree(A) and n > degree(B), therefore using 2
coefficient(C,n) = coefficient(A,n) + coefficient(B,n) = 0 + 0 = 0.
4. Degree of the result of adding two polynomials is bounded above.
5. Therefore has a maximum. (How to do 4->5?!)

Proof document at the same place:
http://sparcs.kaist.ac.kr/~tinuviel/devel/isabelle/PolynomialRing.pdf

-- 
Seo Sanghyeon

PolynomialRing_ZF.thy
Description: Binary data