environ
vocabularies HIDDEN, NUMBERS, RLVECT_1, ALGSTR_0, XBOOLE_0, FINSEQ_1, SUBSET_1, RELAT_1, XXREAL_0, FUNCT_1, SUPINF_2, CARD_3, ARYTM_3, TARSKI, ORDINAL4, PARTFUN1, CARD_1, FUNCT_7, ARYTM_1, RFINSEQ, PRE_POLY, PBOOLE, RELAT_2, BAGORDER, ORDERS_2, WAYBEL_4, ZFMISC_1, XCMPLX_0, ALGSTR_1, LATTICES, POLYNOM7, POLYNOM1, ORDINAL1, VECTSP_2, VALUED_0, VECTSP_1, BINOP_1, POLYRED, REWRITE1, STRUCT_0, MCART_1, TERMORD, GROEB_1, BROUWER, MESFUNC1, CAT_3, GROUP_1, IDEAL_1, FINSET_1, NAT_1, GROEB_2;
notations HIDDEN, TARSKI, RELAT_1, XBOOLE_0, SUBSET_1, RELAT_2, RELSET_1, FUNCT_1, ORDINAL1, XCMPLX_0, PARTFUN1, FINSET_1, XTUPLE_0, MCART_1, XXREAL_0, FINSEQ_1, PRE_POLY, STRUCT_0, ALGSTR_1, VECTSP_2, POLYNOM7, PBOOLE, ORDERS_2, REWRITE1, BAGORDER, ALGSTR_0, RLVECT_1, VFUNCT_1, VECTSP_1, POLYNOM1, TERMORD, IDEAL_1, POLYRED, GROUP_1, NAT_D, NUMBERS, NAT_1, GROEB_1, RFINSEQ, FINSEQ_7, WAYBEL_4, RECDEF_1;
definitions ;
theorems TARSKI, RELSET_1, FINSEQ_1, ZFMISC_1, VECTSP_1, POLYNOM1, FINSEQ_4, RLVECT_1, NAT_1, POLYNOM7, REWRITE1, XBOOLE_0, IDEAL_1, TERMORD, INT_1, FUNCT_1, FINSET_1, XBOOLE_1, VECTSP_2, POLYRED, FUNCT_2, BINOM, FINSEQ_3, RELAT_1, RELAT_2, WAYBEL_4, BAGORDER, RFINSEQ, FINSEQ_5, ALGSTR_1, FINSEQ_7, GROEB_1, GROUP_1, XREAL_1, XXREAL_0, PARTFUN1, VALUED_0, STRUCT_0, NAT_D, PRE_POLY, XTUPLE_0, ORDINAL1;
schemes NAT_1, CLASSES1;
registrations XBOOLE_0, ORDINAL1, FINSET_1, XREAL_0, NAT_1, INT_1, FINSEQ_1, REWRITE1, STRUCT_0, VECTSP_1, ORDERS_2, ALGSTR_1, GCD_1, POLYNOM1, POLYNOM2, POLYNOM4, IDEAL_1, POLYNOM7, TERMORD, POLYRED, VALUED_0, ALGSTR_0, PRE_POLY, CARD_1, VFUNCT_1, FUNCT_1, FUNCT_2, RELSET_1, XTUPLE_0;
constructors HIDDEN, RFINSEQ, REWRITE1, FINSEQ_7, VECTSP_2, WAYBEL_4, WELLFND1, IDEAL_1, BAGORDER, TERMORD, POLYRED, GROEB_1, RECDEF_1, REAL_1, RELSET_1, PBOOLE, BINOP_2, VFUNCT_1, XTUPLE_0;
requirements HIDDEN, NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
equalities STRUCT_0, ALGSTR_0;
expansions STRUCT_0;
definition
let X be
set ;
let b1,
b2 be
bag of
X;
existence
ex b1 being bag of X st
for k being object holds b1 . k = max ((b1 . k),(b2 . k))
uniqueness
for b1, b2 being bag of X st ( for k being object holds b1 . k = max ((b1 . k),(b2 . k)) ) & ( for k being object holds b2 . k = max ((b1 . k),(b2 . k)) ) holds
b1 = b2
commutativity
for b1, b1, b2 being bag of X st ( for k being object holds b1 . k = max ((b1 . k),(b2 . k)) ) holds
for k being object holds b1 . k = max ((b2 . k),(b1 . k))
;
idempotence
for b1 being bag of X
for k being object holds b1 . k = max ((b1 . k),(b1 . k))
;
end;
definition
let X be
set ;
let b1,
b2 be
bag of
X;
end;
theorem Th7:
for
X being
set for
b1,
b2 being
bag of
X holds
(
b2 divides b1 iff
lcm (
b1,
b2)
= b1 )
Lm1:
for n being Ordinal
for T being connected TermOrder of n
for L being non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr
for f being Polynomial of n,L
for g being object
for P being Subset of (Polynom-Ring (n,L)) st PolyRedRel (P,T) reduces f,g holds
g is Polynomial of n,L
theorem Th17:
for
n being
Element of
NAT for
T being
connected admissible TermOrder of
n for
L being non
empty non
degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr for
P being
Subset of
(Polynom-Ring (n,L)) st ( for
p1,
p2 being
Polynomial of
n,
L st
p1 <> p2 &
p1 in P &
p2 in P holds
for
m1,
m2 being
Monomial of
n,
L st
HM (
(m1 *' p1),
T)
= HM (
(m2 *' p2),
T) holds
PolyRedRel (
P,
T)
reduces (m1 *' p1) - (m2 *' p2),
0_ (
n,
L) ) holds
P is_Groebner_basis_wrt T
definition
let n be
Ordinal;
let T be
connected TermOrder of
n;
let L be non
trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr ;
let p1,
p2 be
Polynomial of
n,
L;
func S-Poly (
p1,
p2,
T)
-> Polynomial of
n,
L equals
((HC (p2,T)) * (((lcm ((HT (p1,T)),(HT (p2,T)))) / (HT (p1,T))) *' p1)) - ((HC (p1,T)) * (((lcm ((HT (p1,T)),(HT (p2,T)))) / (HT (p2,T))) *' p2));
coherence
((HC (p2,T)) * (((lcm ((HT (p1,T)),(HT (p2,T)))) / (HT (p1,T))) *' p1)) - ((HC (p1,T)) * (((lcm ((HT (p1,T)),(HT (p2,T)))) / (HT (p2,T))) *' p2)) is Polynomial of n,L
;
end;
::
deftheorem defines
S-Poly GROEB_2:def 4 :
for n being Ordinal
for T being connected TermOrder of n
for L being non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr
for p1, p2 being Polynomial of n,L holds S-Poly (p1,p2,T) = ((HC (p2,T)) * (((lcm ((HT (p1,T)),(HT (p2,T)))) / (HT (p1,T))) *' p1)) - ((HC (p1,T)) * (((lcm ((HT (p1,T)),(HT (p2,T)))) / (HT (p2,T))) *' p2));
Lm2:
for L being non empty add-cancelable right_complementable well-unital distributive add-associative right_zeroed associative left_zeroed doubleLoopStr
for P being Subset of L
for p being Element of L st p in P holds
p in P -Ideal
Lm3:
for n being Ordinal
for T being connected TermOrder of n
for L being non trivial right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr
for p, q being Polynomial of n,L
for f, g being Element of (Polynom-Ring (n,L)) st f = p & g = q holds
f - g = p - q
theorem
for
n being
Ordinal for
T being
connected admissible TermOrder of
n for
L being non
trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr for
p1,
p2 being
Polynomial of
n,
L holds
(
S-Poly (
p1,
p2,
T)
= 0_ (
n,
L) or
HT (
(S-Poly (p1,p2,T)),
T)
< lcm (
(HT (p1,T)),
(HT (p2,T))),
T )
theorem
for
n being
Element of
NAT for
T being
connected admissible TermOrder of
n for
L being non
empty non
degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr for
G being
Subset of
(Polynom-Ring (n,L)) st ( for
g1,
g2,
h being
Polynomial of
n,
L st
g1 in G &
g2 in G &
h is_a_normal_form_of S-Poly (
g1,
g2,
T),
PolyRedRel (
G,
T) holds
h = 0_ (
n,
L) ) holds
for
g1,
g2 being
Polynomial of
n,
L st
g1 in G &
g2 in G holds
PolyRedRel (
G,
T)
reduces S-Poly (
g1,
g2,
T),
0_ (
n,
L)
Lm4:
for n being Ordinal
for T being connected TermOrder of n
for L being non empty non trivial right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr
for f being Polynomial of n,L
for P being non empty Subset of (Polynom-Ring (n,L))
for A being LeftLinearCombination of P st A is_MonomialRepresentation_of f holds
for b being bag of n st ( for i being Element of NAT st i in dom A holds
for m being Monomial of n,L
for p being Polynomial of n,L st A . i = m *' p & p in P holds
(m *' p) . b = 0. L ) holds
f . b = 0. L
Lm5:
for n being Ordinal
for T being connected admissible TermOrder of n
for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr
for f, g being Polynomial of n,L
for f9, g9 being Element of (Polynom-Ring (n,L)) st f = f9 & g = g9 holds
for P being non empty Subset of (Polynom-Ring (n,L)) st PolyRedRel (P,T) reduces f,g holds
ex A being LeftLinearCombination of P st
( f9 = g9 + (Sum A) & ( for i being Element of NAT st i in dom A holds
ex m being non-zero Monomial of n,L ex p being non-zero Polynomial of n,L st
( p in P & A . i = m *' p & HT ((m *' p),T) <= HT (f,T),T ) ) )
theorem
for
n being
Ordinal for
T being
connected TermOrder of
n for
L being non
empty non
trivial right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr for
f,
g being
Polynomial of
n,
L for
P being non
empty Subset of
(Polynom-Ring (n,L)) for
A,
B being
LeftLinearCombination of
P for
b being
bag of
n st
A is_Standard_Representation_of f,
P,
b,
T &
B is_Standard_Representation_of g,
P,
b,
T holds
A ^ B is_Standard_Representation_of f + g,
P,
b,
T
theorem
for
n being
Ordinal for
T being
connected TermOrder of
n for
L being non
empty non
trivial right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr for
f,
g being
Polynomial of
n,
L for
P being non
empty Subset of
(Polynom-Ring (n,L)) for
A,
B being
LeftLinearCombination of
P for
b being
bag of
n for
i being
Element of
NAT st
A is_Standard_Representation_of f,
P,
b,
T &
B = A | i &
g = Sum (A /^ i) holds
B is_Standard_Representation_of f - g,
P,
b,
T
theorem
for
n being
Ordinal for
T being
connected TermOrder of
n for
L being non
empty non
trivial right_complementable well-unital distributive Abelian add-associative right_zeroed doubleLoopStr for
f,
g being
Polynomial of
n,
L for
P being non
empty Subset of
(Polynom-Ring (n,L)) for
A,
B being
LeftLinearCombination of
P for
b being
bag of
n for
i being
Element of
NAT st
A is_Standard_Representation_of f,
P,
b,
T &
B = A /^ i &
g = Sum (A | i) &
i <= len A holds
B is_Standard_Representation_of f - g,
P,
b,
T