Volume 14, 2002

University of Bialystok

Copyright (c) 2002 Association of Mizar Users

### The abstract of the Mizar article:

### Polynomial Reduction

**by****Christoph Schwarzweller**- Received December 20, 2002
- MML identifier: POLYRED

- [ Mizar article, MML identifier index ]

environ vocabulary POLYNOM1, POLYNOM7, BOOLE, FUNCT_1, RELAT_1, VECTSP_1, RLVECT_1, ORDINAL1, LATTICES, ANPROJ_1, VECTSP_2, ALGSTR_1, ARYTM_1, REALSET1, CAT_3, GROUP_1, BINOP_1, ARYTM_3, TERMORD, FINSEQ_4, WELLORD1, IDEAL_1, TARSKI, ORDERS_1, ORDERS_2, RELAT_2, DICKSON, BAGORDER, FINSUB_1, TRIANG_1, MCART_1, REWRITE1, INT_1, FINSEQ_1, WAYBEL_4, FINSET_1, ALGSTR_2, ALGSEQ_1, CARD_1, POLYRED; notation NUMBERS, XCMPLX_0, XREAL_0, TARSKI, XBOOLE_0, SUBSET_1, STRUCT_0, ZFMISC_1, RELAT_1, RELAT_2, MONOID_0, RELSET_1, FUNCT_1, FUNCT_2, ORDINAL1, NAT_1, ALGSTR_1, WAYBEL_0, FINSUB_1, FINSET_1, WAYBEL_4, REWRITE1, RLVECT_1, CARD_1, FINSEQ_1, FINSEQ_4, MCART_1, TRIANG_1, REALSET1, VECTSP_2, VECTSP_1, POLYNOM7, WELLORD1, WELLFND1, IDEAL_1, ORDERS_1, ORDERS_2, POLYNOM1, BAGORDER, TERMORD; constructors ORDERS_2, WAYBEL_4, MONOID_0, REWRITE1, TRIANG_1, IDEAL_1, TERMORD, WELLFND1, DOMAIN_1, MEMBERED, BAGORDER; clusters STRUCT_0, RELAT_1, FINSET_1, RELSET_1, VECTSP_1, FINSEQ_1, VECTSP_2, CARD_1, GCD_1, ALGSTR_1, POLYNOM1, POLYNOM2, REWRITE1, BINOM, FINSUB_1, ORDERS_1, POLYNOM7, BAGORDER, TERMORD, SUBSET_1, IDEAL_1, MONOID_0, NAT_1, XREAL_0, MEMBERED, NUMBERS, ORDINAL2; requirements NUMERALS, REAL, SUBSET, BOOLE; begin :: Preliminaries definition let n be Ordinal, R be non trivial ZeroStr; cluster non-zero Monomial of n,R; end; definition cluster non trivial Field; end; definition cluster Field-like -> domRing-like (left_zeroed add-right-cancelable right-distributive left_unital commutative associative (non empty doubleLoopStr)); end; definition let n be Ordinal, L be add-associative right_complementable left_zeroed right_zeroed unital distributive domRing-like (non trivial doubleLoopStr), p,q be non-zero finite-Support Series of n,L; cluster p *' q -> non-zero; end; begin :: More on Polynomials and Monomials theorem :: POLYRED:1 for X being set, L being Abelian add-associative right_zeroed right_complementable (non empty LoopStr), p,q being Series of X, L holds -(p + q) = (-p) + (-q); theorem :: POLYRED:2 for X being set, L being left_zeroed (non empty LoopStr), p being Series of X, L holds 0_(X,L) + p = p; theorem :: POLYRED:3 for X being set, L being add-associative right_zeroed right_complementable (non empty LoopStr), p being Series of X, L holds -p + p = 0_(X,L) & p + -p = 0_(X,L); theorem :: POLYRED:4 for n being set, L being add-associative right_zeroed right_complementable (non empty LoopStr), p be Series of n, L holds p - 0_(n,L) = p; theorem :: POLYRED:5 for n being Ordinal, L being add-associative right_complementable right_zeroed add-left-cancelable left-distributive (non empty doubleLoopStr), p being Series of n,L holds 0_(n,L) *' p = 0_(n,L); theorem :: POLYRED:6 for n being Ordinal, L being Abelian right_zeroed add-associative right_complementable unital distributive associative commutative (non trivial doubleLoopStr), p,q being Polynomial of n,L holds -(p *' q) = (-p) *' q & -(p *' q) = p *' (-q); theorem :: POLYRED:7 for n being Ordinal, L being add-associative right_complementable right_zeroed distributive (non empty doubleLoopStr), p being Polynomial of n,L, m being Monomial of n,L, b being bag of n holds (m*'p).(term(m)+b) = m.term(m) * p.b; theorem :: POLYRED:8 for X being set, L being right_zeroed add-left-cancelable left-distributive (non empty doubleLoopStr), p being Series of X,L holds 0.L * p = 0_(X,L); theorem :: POLYRED:9 for X being set, L being add-associative right_zeroed right_complementable distributive (non empty doubleLoopStr), p being Series of X,L, a being Element of L holds -(a * p) = (-a) * p & -(a * p) = a * (-p); theorem :: POLYRED:10 for X being set, L being left-distributive (non empty doubleLoopStr), p being Series of X,L, a,a' being Element of L holds a * p + a' * p = (a + a') * p; theorem :: POLYRED:11 for X being set, L being associative (non empty multLoopStr_0), p being Series of X,L, a,a' being Element of L holds (a * a') * p = a * (a' * p); theorem :: POLYRED:12 for n being Ordinal, L being add-associative right_zeroed right_complementable unital associative commutative distributive (non empty doubleLoopStr), p,p' being Series of n,L, a being Element of L holds a * (p *' p') = p *' (a * p'); begin :: Multiplication of polynomials with bags definition let n be Ordinal, b be bag of n, L be non empty ZeroStr, p be Series of n,L; func b *' p -> Series of n,L means :: POLYRED:def 1 for b' being bag of n st b divides b' holds it.b' = p.(b' -' b) & for b' being bag of n st not(b divides b') holds it.b' = 0.L; end; definition let n be Ordinal, b be bag of n, L be non empty ZeroStr, p be finite-Support Series of n,L; cluster b *' p -> finite-Support; end; theorem :: POLYRED:13 for n being Ordinal, b,b' being bag of n, L being non empty ZeroStr, p being Series of n,L holds (b*'p).(b'+b) = p.b'; theorem :: POLYRED:14 for n being Ordinal, L being non empty ZeroStr, p being Polynomial of n,L, b being bag of n holds Support(b*'p) c= {b + b' where b' is Element of Bags n : b' in Support p}; theorem :: POLYRED:15 for n being Ordinal, T being connected admissible TermOrder of n, L being non trivial ZeroStr, p being non-zero Polynomial of n,L, b being bag of n holds HT(b*'p,T) = b + HT(p,T); theorem :: POLYRED:16 for n being Ordinal, T being connected admissible TermOrder of n, L being non empty ZeroStr, p being Polynomial of n,L, b,b' being bag of n holds b' in Support(b*'p) implies b' <= b+HT(p,T),T; theorem :: POLYRED:17 for n being Ordinal, T being connected TermOrder of n, L being non empty ZeroStr, p being Series of n,L holds (EmptyBag n) *' p = p; theorem :: POLYRED:18 for n being Ordinal, T being connected TermOrder of n, L being non empty ZeroStr, p being Series of n,L, b1,b2 being bag of n holds (b1 + b2) *' p = b1 *' (b2 *' p); theorem :: POLYRED:19 for n being Ordinal, L being add-associative right_zeroed right_complementable distributive (non trivial doubleLoopStr), p being Polynomial of n,L, a being Element of L holds Support(a*p) c= Support(p); theorem :: POLYRED:20 for n being Ordinal, L being domRing-like (non trivial doubleLoopStr), p being Polynomial of n,L, a being non-zero Element of L holds Support(p) c= Support(a*p); theorem :: POLYRED:21 for n being Ordinal, T being connected TermOrder of n, L being add-associative right_zeroed right_complementable distributive domRing-like (non trivial doubleLoopStr), p being Polynomial of n,L, a being non-zero Element of L holds HT(a*p,T) = HT(p,T); theorem :: POLYRED:22 for n being Ordinal, L being add-associative right_complementable right_zeroed distributive (non trivial doubleLoopStr), p being Series of n,L, b being bag of n, a being Element of L holds a * (b *' p) = Monom(a,b) *' p; theorem :: POLYRED:23 for n being Ordinal, T being connected admissible TermOrder of n, L being add-associative right_complementable right_zeroed unital distributive domRing-like (non trivial doubleLoopStr), p being non-zero Polynomial of n,L, q being Polynomial of n,L, m being non-zero Monomial of n,L holds HT(p,T) in Support q implies HT(m*'p,T) in Support(m*'q); begin :: Orders on Polynomials definition let n be Ordinal, T be connected TermOrder of n; cluster RelStr(#Bags n, T#) -> connected; end; definition let n be Nat, T be admissible TermOrder of n; cluster RelStr (#Bags n, T#) -> well_founded; end; definition :: according to p. 193 let n be Ordinal, T be connected TermOrder of n, L be non empty ZeroStr, p,q be Polynomial of n,L; pred p <= q,T means :: POLYRED:def 2 [Support p, Support q] in FinOrd RelStr(# Bags n, T#); end; definition let n be Ordinal, T be connected TermOrder of n, L be non empty ZeroStr, p,q be Polynomial of n,L; pred p < q,T means :: POLYRED:def 3 p <= q,T & Support p <> Support q; end; definition let n being Ordinal, T being connected TermOrder of n, L being non empty ZeroStr, p being Polynomial of n,L; func Support(p,T) -> Element of Fin the carrier of RelStr(#Bags n,T#) equals :: POLYRED:def 4 Support(p); end; theorem :: POLYRED:24 ::: according to definition 5.15, p. 194 for n being Ordinal, T being connected TermOrder of n, L being non trivial ZeroStr, p being non-zero Polynomial of n,L holds PosetMax(Support(p,T)) = HT(p,T); theorem :: POLYRED:25 :: theorem 5.12, p. 193 for n being Ordinal, T being connected TermOrder of n, L being non empty LoopStr, p being Polynomial of n,L holds p <= p,T; theorem :: POLYRED:26 :: theorem 5.12, p. 193 for n being Ordinal, T being connected TermOrder of n, L being non empty LoopStr, p,q being Polynomial of n,L holds (p <= q,T & q <= p,T) iff (Support p = Support q); theorem :: POLYRED:27 :: theorem 5.12, p. 193 for n being Ordinal, T being connected TermOrder of n, L being non empty LoopStr, p,q,r being Polynomial of n,L holds (p <= q,T & q <= r,T) implies p <= r,T; theorem :: POLYRED:28 ::: theorem 5.12, p. 193 for n being Ordinal, T being connected TermOrder of n, L being non empty LoopStr, p,q being Polynomial of n,L holds p <= q,T or q <= p,T; theorem :: POLYRED:29 for n being Ordinal, T being connected TermOrder of n, L being non empty LoopStr, p,q being Polynomial of n,L holds p <= q,T iff not(q < p,T); theorem :: POLYRED:30 for n being Ordinal, T being connected TermOrder of n, L being non empty ZeroStr, p being Polynomial of n,L holds 0_(n,L) <= p,T; theorem :: POLYRED:31 for n being Nat, T being admissible connected TermOrder of n, L being add-associative right_complementable right_zeroed unital distributive (non trivial doubleLoopStr), P being non empty Subset of Polynom-Ring(n,L) holds ex p being Polynomial of n,L st p in P & for q being Polynomial of n,L st q in P holds p <= q,T; theorem :: POLYRED:32 ::: according to p. 193 for n being Ordinal, T being connected admissible TermOrder of n, L being add-associative right_complementable right_zeroed (non trivial LoopStr), p,q being Polynomial of n,L holds p < q,T iff (p = 0_(n,L) & q <> 0_(n,L) or HT(p,T) < HT(q,T),T or HT(p,T) = HT(q,T) & Red(p,T) < Red(q,T),T); theorem :: POLYRED:33 ::: exercise 5.16, p. 194 for n being Ordinal, T being connected admissible TermOrder of n, L being add-associative right_complementable right_zeroed (non trivial LoopStr), p being non-zero Polynomial of n,L holds Red(p,T) < HM(p,T),T; theorem :: POLYRED:34 ::: exercise 5.16, p. 194 for n being Ordinal, T being connected TermOrder of n, L being add-associative right_complementable right_zeroed (non trivial LoopStr), p being Polynomial of n,L holds HM(p,T) <= p,T; theorem :: POLYRED:35 for n being Ordinal, T being connected admissible TermOrder of n, L being add-associative right_complementable right_zeroed (non trivial LoopStr), p being non-zero Polynomial of n,L holds Red(p,T) < p,T; begin :: Polynomial Reduction definition ::: definition 5.18 (i), p. 195 let n be Ordinal, T be connected TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive Field-like (non trivial doubleLoopStr), f,p,g be Polynomial of n,L, b be bag of n; pred f reduces_to g,p,b,T means :: POLYRED:def 5 f <> 0_(n,L) & p <> 0_(n,L) & b in Support f & ex s being bag of n st s + HT(p,T) = b & g = f - (f.b/HC(p,T)) * (s *' p); end; definition ::: definition 5.18 (ii), p. 195 let n be Ordinal, T be connected TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive Field-like (non trivial doubleLoopStr), f,p,g be Polynomial of n,L; pred f reduces_to g,p,T means :: POLYRED:def 6 ex b being bag of n st f reduces_to g,p,b,T; end; definition ::: definition 5.18 (iii), p. 196 let n be Ordinal, T be connected TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive Field-like (non trivial doubleLoopStr), f,g be Polynomial of n,L, P be Subset of Polynom-Ring(n,L); pred f reduces_to g,P,T means :: POLYRED:def 7 ex p being Polynomial of n,L st p in P & f reduces_to g,p,T; end; definition ::: definition 5.18 (iv), p. 196 let n be Ordinal, T be connected TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive Field-like (non trivial doubleLoopStr), f,p be Polynomial of n,L; pred f is_reducible_wrt p,T means :: POLYRED:def 8 ex g being Polynomial of n,L st f reduces_to g,p,T; antonym f is_irreducible_wrt p,T; antonym f is_in_normalform_wrt p,T; end; definition ::: definition 5.18 (v), p. 196 let n be Ordinal, T be connected TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive Field-like (non trivial doubleLoopStr), f be Polynomial of n,L, P be Subset of Polynom-Ring(n,L); pred f is_reducible_wrt P,T means :: POLYRED:def 9 ex g being Polynomial of n,L st f reduces_to g,P,T; antonym f is_irreducible_wrt P,T; antonym f is_in_normalform_wrt P,T; end; definition ::: following definition 5.18, p. 196 let n be Ordinal, T be connected TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive Field-like (non trivial doubleLoopStr), f,p,g be Polynomial of n,L; pred f top_reduces_to g,p,T means :: POLYRED:def 10 f reduces_to g,p,HT(f,T),T; end; definition ::: following definition 5.18, p. 196 let n be Ordinal, T be connected TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive Field-like (non trivial doubleLoopStr), f,p be Polynomial of n,L; pred f is_top_reducible_wrt p,T means :: POLYRED:def 11 ex g being Polynomial of n,L st f top_reduces_to g,p,T; end; definition ::: following definition 5.18, p. 196 let n be Ordinal, T be connected TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive Field-like (non trivial doubleLoopStr), f be Polynomial of n,L, P be Subset of Polynom-Ring(n,L); pred f is_top_reducible_wrt P,T means :: POLYRED:def 12 ex p being Polynomial of n,L st p in P & f is_top_reducible_wrt p,T; end; theorem :: POLYRED:36 ::: lemma 5.20 (i), p. 197 for n being Ordinal, T being connected TermOrder of n, L being add-associative right_complementable right_zeroed commutative associative well-unital distributive Field-like (non trivial doubleLoopStr), f being Polynomial of n,L, p being non-zero Polynomial of n,L holds f is_reducible_wrt p,T iff ex b being bag of n st b in Support f & HT(p,T) divides b; theorem :: POLYRED:37 for n being Ordinal, T being connected TermOrder of n, L being add-associative right_complementable right_zeroed commutative associative well-unital distributive Field-like (non trivial doubleLoopStr), p being Polynomial of n,L holds 0_(n,L) is_irreducible_wrt p,T; theorem :: POLYRED:38 ::: lemma 5.20 (ii), p. 197 for n being Ordinal, T being admissible connected TermOrder of n, L being add-associative right_complementable right_zeroed commutative associative well-unital distributive Abelian Field-like non degenerated (non empty doubleLoopStr), f,p being Polynomial of n,L, m being non-zero Monomial of n,L holds f reduces_to f-m*'p,p,T implies HT(m*'p,T) in Support f; theorem :: POLYRED:39 ::: lemma 5.20 (iii), p. 197 for n being Ordinal, T being connected TermOrder of n, L being add-associative right_complementable right_zeroed commutative associative well-unital distributive Field-like non degenerated (non empty doubleLoopStr), f,p,g being Polynomial of n,L, b being bag of n holds f reduces_to g,p,b,T implies not(b in Support g); theorem :: POLYRED:40 ::: lemma 5.20 (iii), p. 197 for n being Ordinal, T being connected admissible TermOrder of n, L being add-associative right_complementable right_zeroed commutative associative well-unital distributive Field-like (non trivial doubleLoopStr), f,p,g being Polynomial of n,L, b,b' being bag of n st b < b',T holds f reduces_to g,p,b,T implies (b' in Support g iff b' in Support f); theorem :: POLYRED:41 for n being Ordinal, T being connected admissible TermOrder of n, L being add-associative right_complementable right_zeroed commutative associative well-unital distributive Field-like (non trivial doubleLoopStr), f,p,g being Polynomial of n,L, b,b' being bag of n st b < b',T holds f reduces_to g,p,b,T implies f.b' = g.b'; theorem :: POLYRED:42 for n being Ordinal, T being connected admissible TermOrder of n, L being add-associative right_complementable right_zeroed commutative associative well-unital distributive Field-like non degenerated (non empty doubleLoopStr), f,p,g being Polynomial of n,L holds f reduces_to g,p,T implies for b being bag of n st b in Support g holds b <= HT(f,T),T; theorem :: POLYRED:43 ::: lemma 5.20 (iv), p. 197 for n being Ordinal, T being connected admissible TermOrder of n, L being Abelian add-associative right_complementable right_zeroed commutative associative well-unital distributive Field-like non degenerated (non empty doubleLoopStr), f,p,g being Polynomial of n,L holds f reduces_to g,p,T implies g < f,T; begin :: Polynomial Reduction Relation definition let n be Ordinal, T be connected TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive Field-like (non trivial doubleLoopStr), P be Subset of Polynom-Ring(n,L); func PolyRedRel(P,T) -> Relation of (the carrier of Polynom-Ring(n,L)) \ {0_(n,L)}, the carrier of Polynom-Ring(n,L) means :: POLYRED:def 13 for p,q being Polynomial of n,L holds [p,q] in it iff p reduces_to q,P,T; end; theorem :: POLYRED:44 ::: lemma 5.20 (v), p. 197 for n being Ordinal, T being connected admissible TermOrder of n, L being Abelian add-associative right_complementable right_zeroed commutative associative well-unital distributive Field-like non degenerated (non empty doubleLoopStr), f,g being Polynomial of n,L, P being Subset of Polynom-Ring(n,L) holds PolyRedRel(P,T) reduces f,g implies g <= f,T & (g = 0_(n,L) or HT(g,T) <= HT(f,T),T); definition ::: theorem 5.21, p. 198 let n be Nat, T be connected admissible TermOrder of n, L be Abelian add-associative right_complementable right_zeroed commutative associative well-unital distributive Field-like non degenerated (non empty doubleLoopStr), P be Subset of Polynom-Ring(n,L); cluster PolyRedRel(P,T) -> strongly-normalizing; end; theorem :: POLYRED:45 ::: lemma 5.24 (i), p. 200 for n being Nat, T being admissible connected TermOrder of n, L being add-associative right_complementable left_zeroed right_zeroed commutative associative well-unital distributive Abelian Field-like (non trivial doubleLoopStr), P being Subset of Polynom-Ring(n,L), f,h being Polynomial of n,L holds f in P implies PolyRedRel(P,T) reduces h*'f,0_(n,L); theorem :: POLYRED:46 ::: lemma 5.24 (ii), p. 200 for n being Ordinal, T being connected admissible TermOrder of n, L being Abelian add-associative right_complementable right_zeroed commutative associative well-unital distributive Field-like non degenerated (non empty doubleLoopStr), P being Subset of Polynom-Ring(n,L), f,g being Polynomial of n,L, m being non-zero Monomial of n,L holds f reduces_to g,P,T implies m*'f reduces_to m*'g,P,T; theorem :: POLYRED:47 ::: lemma 5.24 (iii), p. 200 for n being Ordinal, T being connected admissible TermOrder of n, L being Abelian add-associative right_complementable right_zeroed commutative associative well-unital distributive Field-like non degenerated (non empty doubleLoopStr), P being Subset of Polynom-Ring(n,L), f,g being Polynomial of n,L, m being Monomial of n,L holds PolyRedRel(P,T) reduces f,g implies PolyRedRel(P,T) reduces m*'f,m*'g; theorem :: POLYRED:48 ::: lemma 5.24 (iii), p. 200 for n being Ordinal, T being connected admissible TermOrder of n, L being Abelian add-associative right_complementable right_zeroed commutative associative well-unital distributive Field-like non degenerated (non empty doubleLoopStr), P being Subset of Polynom-Ring(n,L), f being Polynomial of n,L, m being Monomial of n,L holds PolyRedRel(P,T) reduces f,0_(n,L) implies PolyRedRel(P,T) reduces m*'f,0_(n,L); theorem :: POLYRED:49 ::: lemma 5.25 (i), p. 200 for n being Ordinal, T being connected TermOrder of n, L being add-associative right_complementable right_zeroed commutative associative well-unital distributive Abelian Field-like (non trivial doubleLoopStr), P being Subset of Polynom-Ring(n,L), f,g,h,h1 being Polynomial of n,L holds (f - g = h & PolyRedRel(P,T) reduces h,h1) implies ex f1,g1 being Polynomial of n,L st f1 - g1 = h1 & PolyRedRel(P,T) reduces f,f1 & PolyRedRel(P,T) reduces g,g1; theorem :: POLYRED:50 ::: lemma 5.25 (ii), p. 200 for n being Ordinal, T being connected TermOrder of n, L being add-associative right_complementable right_zeroed commutative associative well-unital distributive Abelian Field-like (non trivial doubleLoopStr), P being Subset of Polynom-Ring(n,L), f,g being Polynomial of n,L holds PolyRedRel(P,T) reduces f-g,0_(n,L) implies f,g are_convergent_wrt PolyRedRel(P,T); theorem :: POLYRED:51 ::: lemma 5.25 (ii), p. 200 for n being Ordinal, T being connected TermOrder of n, L being add-associative right_complementable right_zeroed commutative associative well-unital distributive Abelian Field-like (non trivial doubleLoopStr), P being Subset of Polynom-Ring(n,L), f,g being Polynomial of n,L holds PolyRedRel(P,T) reduces f-g,0_(n,L) implies f,g are_convertible_wrt PolyRedRel(P,T); definition let R be non empty LoopStr, I be Subset of R, a,b be Element of R; pred a,b are_congruent_mod I means :: POLYRED:def 14 a - b in I; end; theorem :: POLYRED:52 for R being add-associative left_zeroed right_zeroed right_complementable right-distributive (non empty doubleLoopStr), I being right-ideal (non empty Subset of R), a being Element of R holds a,a are_congruent_mod I; theorem :: POLYRED:53 for R being add-associative right_zeroed right_complementable right_unital right-distributive (non empty doubleLoopStr), I being right-ideal (non empty Subset of R), a,b being Element of R holds a,b are_congruent_mod I implies b,a are_congruent_mod I; theorem :: POLYRED:54 for R being add-associative right_zeroed right_complementable (non empty LoopStr), I being add-closed (non empty Subset of R), a,b,c being Element of R holds a,b are_congruent_mod I & b,c are_congruent_mod I implies a,c are_congruent_mod I; theorem :: POLYRED:55 for R being Abelian add-associative right_zeroed right_complementable unital distributive associative (non trivial doubleLoopStr), I being add-closed (non empty Subset of R), a,b,c,d being Element of R holds a,b are_congruent_mod I & c,d are_congruent_mod I implies a+c,b+d are_congruent_mod I; theorem :: POLYRED:56 for R being add-associative right_zeroed right_complementable commutative distributive (non empty doubleLoopStr), I being add-closed right-ideal (non empty Subset of R), a,b,c,d being Element of R holds a,b are_congruent_mod I & c,d are_congruent_mod I implies a*c,b*d are_congruent_mod I; theorem :: POLYRED:57 ::: lemma 5.26, p. 202 for n being Ordinal, T being connected TermOrder of n, L being Abelian add-associative right_complementable right_zeroed commutative associative well-unital distributive Field-like (non trivial doubleLoopStr), P being Subset of Polynom-Ring(n,L), f,g being Element of Polynom-Ring(n,L) holds f,g are_convertible_wrt PolyRedRel(P,T) implies f,g are_congruent_mod P-Ideal; theorem :: POLYRED:58 ::: lemma 5.26, p. 202 for n being Nat, T being admissible connected TermOrder of n, L being Abelian add-associative right_complementable right_zeroed commutative associative well-unital distributive Field-like non degenerated (non empty doubleLoopStr), P being non empty Subset of Polynom-Ring(n,L), f,g being Element of Polynom-Ring(n,L) holds f,g are_congruent_mod P-Ideal implies f,g are_convertible_wrt PolyRedRel(P,T); theorem :: POLYRED:59 ::: lemma 5.26, p. 202 for n being Ordinal, T being connected TermOrder of n, L being Abelian add-associative right_complementable right_zeroed commutative associative well-unital distributive Field-like (non trivial doubleLoopStr), P being Subset of Polynom-Ring(n,L), f,g being Polynomial of n,L holds PolyRedRel(P,T) reduces f,g implies f-g in P-Ideal; theorem :: POLYRED:60 ::: lemma 5.26, p. 202 for n being Ordinal, T being connected TermOrder of n, L being Abelian add-associative right_complementable right_zeroed commutative associative well-unital distributive Field-like (non trivial doubleLoopStr), P being Subset of Polynom-Ring(n,L), f being Polynomial of n,L holds PolyRedRel(P,T) reduces f,0_(n,L) implies f in P-Ideal;

Back to top