2 Lemmas
Lemma
15
monic_leadingTerm
Lemma
16
support_leadingTerm
Lemma
17
support_leadingTerm’
Lemma
18
le_degree_of_mem_support
Lemma
19
leadingTerm_eq_leadingTerm_iff
Lemma
21
monic_of_subsingleton
Lemma
22
degree_le_degree_of_support_subset
Theorem
23
degree_mul_le’
Theorem
24
leadingCoeff_mul’
Lemma
25
degree_rename_killCompl_le_degree
Lemma
26
toWithBotSyn_apply_bot
Lemma
27
toWithBotSyn_symm_apply_bot
Lemma
28
toWithBotSyn_apply_eq_bot_iff
Lemma
29
toWithBotSyn_apply_le_bot_iff
Lemma
30
toWithBotSyn_apply_coe
Lemma
31
bot_lt_toWithBotSyn_apply_iff
Lemma
32
toWithBotSyn_symm_apply_eq_bot
Lemma
33
toWithBotSyn_apply
Lemma
34
withBotDegree_eq
Lemma
35
withBotDegree_eq_coe_degree_iff
Lemma
36
withBotDegree_eq_bot_iff
Lemma
37
degree_eq_unbotD_withBotDegree
Lemma
38
withBotDegree_zero
Lemma
39
withBotDegree_monomial
Lemma
41
withBotDegree_leadingTerm
Lemma
42
withBotDegree_neg
Lemma
43
withBotDegree_one
Lemma
44
mem_nonZeroDivisors_of_leadingCoeff_mem_nonZeroDivisors
Lemma
45
withBotDegree_mul_of_left_mem_nonZeroDivisors
Lemma
46
withBotDegree_mul_of_right_mem_nonZeroDivisors
Lemma
47
withBotDegree_mul
Lemma
48
withBotDegree_mul_le
Lemma
49
withBotDegree_mul_le’
Lemma
50
withBotDegree_le_withBotDegree_iff
Lemma
51
withBotDegree_le_withBotDegree_iff_of_ne_zero
Lemma
52
withBotDegree_lt_withBotDegree_iff
Lemma
53
withBotDegree_lt_withBotDegree_iff_of_ne_zero
Lemma
54
withBotDegree_eq_withBotDegree_iff
Lemma
55
withBotDegree_add_le
Lemma
56
withBotDegree_add_of_lt
Lemma
57
withBotDegree_add_of_right_lt
Lemma
58
withBotDegree_sum_le
Lemma
59
le_withBotDegree
Lemma
60
withBotDegree_le_withBotDegree_of_support_subset
Lemma
61
withBotDegree_rename_killCompl_le_withBotDegree
Theorem
62
isRemainder_def’
A variant of MonomialOrder.IsRemainder without coercion of a Set (MvPolynomial σ R).
Theorem
63
isRemainder_def’’
A variant of MonomialOrder.IsRemainder where g : MvPolynomial σ R →₀ MvPolynomial σ R is replaced with a function g : MvPolynomial σ R → MvPolynomial σ R without limitation on its support.
Theorem
64
isRemainder_finset
A variant of MonomialOrder.IsRemainder_def where B is Finset (MvPolynomial σ R).
Theorem
65
isRemainder_range
r is a remainder of a family of polynomials, if and only if it is a remainder with properities defined in MonomialOrder.div with this family of polynomials given as a map from indexes to them.
It is a variant of MonomialOrder.IsRemainder where divisors are given as a map from indexes to polynomials.
Theorem
66
isRemainder_range_fintype
Theorem
67
isRemainder_insert_zero_iff_isRemainder
Remainders are preserved on insertion of the zero polynomial into the set of divisors.
Theorem
68
isRemainder_sdiff_singleton_zero_iff_isRemainder
Remainders are preserved with the zero polynomial removed from the set of divisors.
Theorem
69
isRemainder_zero
Theorem
70
isRemainder_zero_iff
Theorem
71
isRemainder_iff_degree
Lemma
72
mem_ideal_of_mem_ideal
Lemma
73
term_notMem_span_leadingTerm
Lemma
74
term_notMem_span_leadingTerm₀
Lemma
75
monomial_notMem_span_leadingTerm
Lemma
76
MonomialOrder.IsRemainder.monomial_notMem_span_leadingTerm
Lemma
77
monomial_notMem_span_leadingTerm₀
Lemma
78
withBotDegree_remainder_le
Lemma
79
exists_withBotDegree_le_degree
Lemma
80
exists_degree_le_degree_of_zero
Lemma
81
MonomialOrder.IsRemainder.of_subsingleton
Lemma
82
isRemainder_killCompl_of_isRemainder_rename
Lemma
83
isRemainder_rename_of_isRemainder
Lemma
84
isRemainder_iff_isRemainder_rename
Theorem
85
exists_isRemainder
Theorem
86
exists_isRemainder₀
A variant of div_set including 0
Lemma
88
sub_mem_ideal_of_isRemainder_of_subset_ideal
Lemma
89
sub_monomial_notMem_span_leadingTerm
Theorem
90
exists_isRemainder’
A variant of div_set in field
Lemma
91
term_notMem_span_leadingTerm’
Theorem
92
WellFoundedLT.toWellFoundedRelation.congr_simp
Lemma
93
isGroebnerBasis_self
Lemma
94
isGroebnerBasis_sdiff_singleton_zero
Lemma
95
isGroebnerBasis_insert_zero
Theorem
96
exists_isGroebnerBasis_finite
Finite Gröbner basis exists for any ideal of a noetherian multivariate polynomial ring.
Lemma
97
singleton_zero_bot
Lemma
99
singleton_zero_iff
Lemma
101
MonomialOrder.IsGroebnerBasis.of_subsingleton
Theorem
102
isGroebnerBasis_iff_subset_and_degree_le_eq_and_degree_le
Theorem
103
span_leadingTerm_eq_span_monomial
Theorem
104
span_leadingTerm_eq_span_monomial₀
Theorem
105
remainder_eq_zero_iff_mem_ideal
Given a remainder r of a polynomial p on division by a Gröbner basis G of an ideal I, the remainder r is 0 if and only if p is in the ideal I.
Any leading coefficient of polynomial in the Gröbner basis G is required to be a unit.
Theorem
106
remainder_eq_zero_iff_mem_ideal₀
Given a remainder r of a polynomial p on division by a Gröbner basis G of an ideal I, the remainder r is 0 if and only if p is in the ideal I.
It is a variant of MonomialOrder.IsGroebnerBasis.remainder_eq_zero_iff_mem_ideal, allowing the Gröbner basis to contain also 0, besides polynomials with invertible leading coefficients.
Theorem
107
isRemainder_zero_iff_mem_ideal
Given a Gröbner basis G of an ideal I, 0 is a remainder on division by G if and only if p is in the ideal I.
Lemma
108
isRemainder_zero_iff_mem_ideal₀
Theorem
109
ideal_eq_span
Gröbner basis of any ideal spans the ideal.
Theorem
110
isGroebnerBasis_iff_ideal_eq_span_and_isGroebnerBasis_span
Theorem
111
isGroebnerBasis_iff_ideal_eq_span_and_isGroebnerBasis_span₀
Theorem
112
isGroebnerBasis_iff_subset_ideal_and_isRemainder_zero
A set of polynomials is a Gröbner basis of an ideal if and only if it is a subset of this ideal and 0 is a remainder of each member of this ideal on division by this set.
Any leading coefficient of polynomial in the set is required to be a unit.
Theorem
113
isGroebnerBasis_iff_subset_ideal_and_isRemainder_zero₀
A set of polynomials is a Gröbner basis of an ideal if and only if it is a subset of this ideal and 0 is a remainder of each member of this ideal on division by this set.
It is a variant of MonomialOrder.IsGroebnerBasis.isGroebnerBasis_iff_subset_ideal_and_isRemainder_zero, allowing the set to contain also 0, besides polynomials with invertible leading coefficients.
Theorem
114
existsUnique_isRemainder
Remainder of any polynomial on division by a Gröbner basis exists and is unique.
Any leading coefficient of polynomial in the Gröbner basis is required to be a unit.
Theorem
115
existsUnique_isRemainder₀
Remainder of any polynomial on division by a Gröbner basis exists and is unique.
It is a variant of MonomialOrder.IsGroebnerBasis.existsUnique_isRemainder, allowing the Gröbner basis to contain also 0, besides polynomials with invertible leading coefficients.
Theorem
116
remainder_eq_zero_iff_mem_ideal’
Given a remainder r of a polynomial p on division by a Gröbner basis G of an ideal I, the remainder r is 0 if and only if p is in the ideal I.
It is a variant of MonomialOrder.IsGroebnerBasis.remainder_eq_zero_iff_mem_ideal, over a field and without hypothesis on leading coefficients in the Gröbner basis.
Lemma
117
isRemainder_zero_iff_mem_ideal’
Theorem
118
isGroebnerBasis_iff_subset_ideal_and_isRemainder_zero’
A set of polynomials is a Gröbner basis of an ideal if and only if it is a subset of this ideal and 0 is a remainder of each member of this ideal on division by this set.
It is a variant of MonomialOrder.IsGroebnerBasis.isGroebnerBasis_iff_subset_ideal_and_isRemainder_zero, over a field and without hypothesis on leading coefficients in the set.
Theorem
119
isGroebnerBasis_iff_isRemainder_sPolynomial_zero
Buchberger Criterion: a basis of an ideal is a Gröbner basis of it if and only if 0 is a remainder of echo sPolynomial between two polynomials on the basis.
Theorem
120
isGroebnerBasis_iff_isRemainder_sPolynomial_zero’
Buchberger Criterion: a basis of an ideal is a Gröbner basis of it if and only if any remainder of echo sPolynomial between two polynomials on the basis is 0.
It is a variant of MonomialOrder.IsGroebnerBasis.isGroebnerBasis_iff_isRemainder_sPolynomial_zero.
Theorem
121
isGroebnerBasis_iff_ideal_eq_span_and_isGroebnerBasis_span’
Lemma
122
isGroebnerBasis_iff_isGroebnerBasis_rename
Lemma
123
exists_isGroebnerBasis_finite_of_exists_span_finite
Lemma
124
isGroebnerBasis_of_forall_finite_isGroebnerBasis
Theorem
125
MonomialOrder.IsGroebnerBasis.IsReduced.congr_simp
Theorem
126
MonomialOrder.IsGroebnerBasis.IsMinimal.congr_simp
Lemma
127
isGroebnerBasis_minimal
Lemma
128
isGroebnerBasis_monomial
Lemma
129
isGroebnerBasis_monomial_minimal
Lemma
133
span_image_leadingTerm
Lemma
139
MonomialOrder.IsGroebnerBasis.IsReduced.of_subsingleton
Lemma
140
MonomialOrder.IsGroebnerBasis.IsMinimal.of_subsingleton
Lemma
141
isReduced_monomial
Lemma
142
image_leadingTerm_eq_image_monomial_one
Lemma
143
isReduced_leadingTerm
Lemma
144
isGroebnerBasis_of_isMinimal_leadingTerm
Lemma
147
isMinimal_iff_monic_and_minimal_degree_and_injOn_leadingTerm
Lemma
148
degree_image_eq_setOf_minimal
Lemma
149
degree_image_eq_of_isMinimal
Lemma
150
isMinimal_of_isMinimal_leadingTerm
Lemma
151
leadingCoeff_add_of_lt_right
Lemma
153
degree_le_mul_left
Lemma
154
isGroebnerBasis_image_isRemainder
Lemma
155
isReduced_image_isRemainder_of_IsMinimal
Lemma
156
exists_of_isGroebnerBasis
Lemma
157
exists_of_isGroebnerBasis₀
Lemma
158
exists_of_isGroebnerBasis’
Theorem
159
uniqueExists_of_isGroebnerBasis
Theorem
160
uniqueExists_of_isGroebnerBasis₀
Theorem
161
uniqueExists_of_isGroebnerBasis’