begin
theorem Th1:
theorem
for
n being
Ordinal for
T being
connected admissible TermOrder of
n for
L being non
empty non
degenerated right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr for
f,
p,
g being
Polynomial of
n,
L st
f reduces_to g,
p,
T holds
ex
m being
Monomial of
n,
L st
(
g = f - (m *' p) & not
HT (m *' p),
T in Support g &
HT (m *' p),
T <= HT f,
T,
T )
Lm1:
for L being non empty add-cancelable right_complementable associative well-unital distributive add-associative right_zeroed left_zeroed doubleLoopStr
for P being Subset of L
for p being Element of L st p in P holds
p in P -Ideal
Lm2:
for n being Ordinal
for T being connected admissible TermOrder of n
for L being non empty non degenerated right_complementable almost_left_invertible associative commutative 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
Lm3:
for n being Ordinal
for T being connected TermOrder of n
for L being non trivial right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr
for f being Polynomial of n,L holds f is_irreducible_wrt 0_ n,L,T
theorem Th3:
theorem Th4:
theorem Th5:
theorem Th6:
theorem Th7:
theorem Th8:
theorem Th9:
begin
theorem Th10:
theorem
:: deftheorem defines HT GROEB_1:def 1 :
:: deftheorem defines multiples GROEB_1:def 2 :
theorem
theorem
theorem
Lm4:
for n being Ordinal
for T being connected TermOrder of n
for L being non trivial right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr
for f being Polynomial of n,L
for g being set
for P being Subset of (Polynom-Ring n,L) st PolyRedRel P,T reduces f,g holds
g is Polynomial of n,L
Lm5:
for n being Ordinal
for T being connected TermOrder of n
for L being non trivial right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr
for f, g being Polynomial of n,L
for P being Subset of (Polynom-Ring n,L) st PolyRedRel P,T reduces f,g & g <> f holds
ex h being Polynomial of n,L st
( f reduces_to h,P,T & PolyRedRel P,T reduces h,g )
theorem Th15:
theorem Th16:
theorem Th17:
theorem Th18:
theorem
theorem
:: deftheorem Def3 defines is_Groebner_basis_wrt GROEB_1:def 3 :
:: deftheorem Def4 defines is_Groebner_basis_of GROEB_1:def 4 :
Lm6:
for n being Ordinal
for T being connected TermOrder of n
for L being non trivial right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr
for P being Subset of (Polynom-Ring n,L)
for a, b being set st a <> b & PolyRedRel P,T reduces a,b holds
( a is Polynomial of n,L & b is Polynomial of n,L )
theorem
theorem
theorem
Lm7:
for n being Ordinal
for T being connected TermOrder of n
for L being non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for I being LeftIdeal of (Polynom-Ring n,L)
for G being non empty Subset of (Polynom-Ring n,L) st G c= I & ( for f being Polynomial of n,L st f in I holds
PolyRedRel G,T reduces f, 0_ n,L ) holds
G -Ideal = I
theorem Th24:
theorem Th25:
theorem Th26:
theorem Th27:
theorem Th28:
theorem Th29:
begin
theorem Th30:
theorem
theorem
theorem
Lm8:
for n being Ordinal
for b1, b2, b3 being bag of n st b1 divides b2 & b2 divides b3 holds
b1 divides b3
:: deftheorem Def5 defines DivOrder GROEB_1:def 5 :
theorem Th34:
theorem Th35:
Lm9:
for L being non empty right_complementable associative well-unital distributive add-associative right_zeroed left_zeroed doubleLoopStr
for A, B being non empty Subset of L st B = A \ {(0. L)} holds
for f being LinearCombination of A
for u being set st u = Sum f holds
ex g being LinearCombination of B st u = Sum g
theorem
:: deftheorem Def6 defines is_monic_wrt GROEB_1:def 6 :
:: deftheorem Def7 defines is_reduced_wrt GROEB_1:def 7 :
theorem Th37:
for
n being
Ordinal for
T being
connected admissible TermOrder of
n for
L being non
empty non
degenerated right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr for
I being
add-closed left-ideal Subset of
(Polynom-Ring n,L) for
m being
Monomial of
n,
L for
f,
g being
Polynomial of
n,
L st
f in I &
g in I &
HM f,
T = m &
HM g,
T = m & ( for
p being
Polynomial of
n,
L holds
( not
p in I or not
p < f,
T or not
HM p,
T = m ) ) & ( for
p being
Polynomial of
n,
L holds
( not
p in I or not
p < g,
T or not
HM p,
T = m ) ) holds
f = g
Lm10:
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 associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for p being Polynomial of n,L
for I being non empty add-closed left-ideal Subset of (Polynom-Ring n,L) st p in I & p <> 0_ n,L holds
ex q being Polynomial of n,L st
( q in I & HM q,T = Monom (1. L),(HT p,T) & q <> 0_ n,L )
theorem
theorem
theorem