2 Lemmas
Lemma
12
monic_leadingTerm
Lemma
13
support_leadingTerm
Lemma
14
support_leadingTerm’
Lemma
15
le_degree_of_mem_support
Lemma
16
leadingTerm_eq_leadingTerm_iff
Lemma
18
monic_of_subsingleton
Lemma
19
degree_le_degree_of_support_subset
Theorem
20
degree_mul_le’
Lemma
21
mem_nonZeroDivisors_of_leadingCoeff_mem_nonZeroDivisors
Theorem
22
leadingCoeff_mul’
Lemma
23
sPolynomial_decomposition_of_degree_sum_smul_le₀
Lemma
24
sPolynomial_decomposition_of_degree_sum_smul_le
Lemma
25
sPolynomial_decomposition_of_degree_sum_le
Lemma
26
sPolynomial_monomial_mul_of_mem_nonZeroDivisors
Lemma
27
sPolynomial_monomial_mul_of_mem_nonZeroDivisors’
Theorem
28
leadingCoeff_mul_of_left_mem_nonZeroDivisors’
Theorem
29
leadingCoeff_mul_of_right_mem_nonZeroDivisors’
Lemma
30
support_add_of_leadingTerm_add_leadingTerm_eq_zero
Lemma
32
support_sub_of_leadingTerm_eq_leadingTerm
Lemma
33
degree_rename_killCompl_le_degree
Lemma
34
toWithBotSyn_apply_bot
Lemma
35
toWithBotSyn_symm_apply_bot
Lemma
36
toWithBotSyn_apply_eq_bot_iff
Lemma
37
toWithBotSyn_apply_le_bot_iff
Lemma
38
toWithBotSyn_apply_coe
Lemma
39
bot_lt_toWithBotSyn_apply_iff
Lemma
40
toWithBotSyn_symm_apply_eq_bot
Lemma
41
toWithBotSyn_apply
Lemma
42
withBotDegree_eq
Lemma
43
withBotDegree_eq_coe_degree_iff
Lemma
44
withBotDegree_eq_bot_iff
Lemma
45
degree_eq_unbotD_withBotDegree
Lemma
46
withBotDegree_zero
Lemma
47
withBotDegree_monomial
Lemma
49
withBotDegree_leadingTerm
Lemma
50
withBotDegree_neg
Lemma
51
withBotDegree_one
Lemma
52
withBotDegree_mul_of_left_mem_nonZeroDivisors
Lemma
53
withBotDegree_mul_of_right_mem_nonZeroDivisors
Lemma
54
withBotDegree_mul
Lemma
55
withBotDegree_mul_le
Lemma
56
withBotDegree_mul_le’
Lemma
57
withBotDegree_le_withBotDegree_iff
Lemma
58
withBotDegree_le_withBotDegree_iff’
Lemma
59
withBotDegree_le_withBotDegree_iff_of_ne_zero
Lemma
60
withBotDegree_lt_withBotDegree_iff
Lemma
61
withBotDegree_lt_withBotDegree_iff_of_ne_zero
Lemma
62
withBotDegree_eq_withBotDegree_iff
Lemma
63
withBotDegree_add_le
Lemma
64
withBotDegree_add_of_lt
Lemma
65
withBotDegree_add_of_right_lt
Lemma
66
withBotDegree_sum_le
Lemma
67
le_withBotDegree
Lemma
68
withBotDegree_le_withBotDegree_of_support_subset
Lemma
69
withBotDegree_rename_killCompl_le_withBotDegree
Theorem
70
isRemainder_def
Theorem
71
isRemainder_def’
A variant of MonomialOrder.IsRemainder without coercion of a Set (MvPolynomial σ R).
Theorem
72
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
73
isRemainder_finset
A variant of MonomialOrder.IsRemainder_def where B is Finset (MvPolynomial σ R).
Theorem
74
isRemainder_iff_exists_isRemainder_finset
Theorem
75
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
76
isRemainder_range_fintype
Theorem
77
isRemainder_insert_zero_iff_isRemainder
Remainders are preserved on insertion of the zero polynomial into the set of divisors.
Theorem
78
isRemainder_sdiff_singleton_zero_iff_isRemainder
Remainders are preserved with the zero polynomial removed from the set of divisors.
Theorem
79
isRemainder_zero
Theorem
80
isRemainder_zero_iff
Theorem
81
isRemainder_iff_degree
Theorem
82
isRemainder_iff_degree₀
Lemma
83
mem_ideal_of_mem_ideal
Lemma
84
term_notMem_span_span_monomial
Lemma
85
term_notMem_span_leadingTerm
Lemma
86
monomial_notMem_span_monomial
Lemma
87
monomial_notMem_span_leadingTerm
Lemma
88
withBotDegree_remainder_le
Lemma
89
exists_withBotDegree_le_withBotDegree
Lemma
90
exists_withBotDegree_le_withBotDegree₀
Lemma
91
withBotDegree_eq_withBotDegree_iff_leadingTerm_eq_leadingTerm
Lemma
92
exists_degree_le_degree_of_zero
Lemma
93
MonomialOrder.IsRemainder.of_subsingleton
Lemma
94
isRemainder_killCompl_of_isRemainder_rename
Lemma
95
isRemainder_rename_of_isRemainder
Lemma
96
isRemainder_iff_isRemainder_rename
Theorem
97
exists_isRemainder
Theorem
98
exists_isRemainder₀
A variant of div_set including 0
Lemma
100
sub_mem_ideal_of_isRemainder_of_subset_ideal
Lemma
101
sub_monomial_notMem_span_leadingTerm
Theorem
102
exists_isRemainder’
A variant of div_set in field
Theorem
103
isRemainder_iff_degree’
Lemma
105
span_leadingTerm_image
Lemma
106
isGroebnerBasis_iff
Lemma
108
isGroebnerBasis_self
Lemma
109
isGroebnerBasis_sdiff_singleton_zero
Lemma
110
isGroebnerBasis_insert_zero
Theorem
111
exists_isGroebnerBasis_finite
Finite Gröbner basis exists for any ideal of a noetherian multivariate polynomial ring.
Lemma
112
singleton_zero_bot
Lemma
114
singleton_zero_iff
Lemma
116
MonomialOrder.IsGroebnerBasis.of_subsingleton
Theorem
117
isGroebnerBasis_iff_subset_and_degree_le_eq_and_degree_le
Lemma
118
isGroebnerBasis_iff_subset_and_degree_le_eq_and_degree_le₀
Lemma
119
span_leadingTerm_eq_span_monomial
Theorem
120
span_leadingTerm_eq_span_monomial₀
Lemma
121
isGroebnerBasis_of_forall_finite_isGroebnerBasis₀
Theorem
122
isGroebnerBasis_union_of_forall_finite_isGroebnerBasis₀
Lemma
123
isGroebnerBasis_of_forall_finite_isGroebnerBasis
Theorem
124
isGroebnerBasis_union_of_forall_finite_isGroebnerBasis
Theorem
125
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
126
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
127
isRemainder_zero_iff_mem_ideal₀
Theorem
128
ideal_eq_span
Gröbner basis of any ideal spans the ideal.
Theorem
129
ideal_eq_span₀
Theorem
130
isGroebnerBasis_iff_ideal_eq_span_and_isGroebnerBasis_span
Theorem
131
isGroebnerBasis_iff_ideal_eq_span_and_isGroebnerBasis_span₀
Theorem
132
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
133
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
134
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
135
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
136
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
137
isGroebnerBasis_iff_isRemainder_sPolynomial_zero₀
Theorem
138
isGroebnerBasis_iff_forall_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.
Lemma
139
isGroebnerBasis_iff_isGroebnerBasis_rename
Lemma
140
isGroebnerBasis_iff_isGroebnerBasis_rename₀
Theorem
141
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.
Lemma
142
isRemainder_zero_iff_mem_ideal’
Theorem
143
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
144
isGroebnerBasis_iff_ideal_eq_span_and_isGroebnerBasis_span’
Theorem
145
isGroebnerBasis_iff_subset_and_degree_le_eq_and_degree_le’
Lemma
146
isGroebnerBasis_iff_isGroebnerBasis_rename’
Lemma
147
exists_isGroebnerBasis_finite_of_exists_span_finite
Lemma
148
isGroebnerBasis_of_forall_finite_isGroebnerBasis’
Theorem
149
isGroebnerBasis_union_of_forall_finite_isGroebnerBasis’
Lemma
150
isGroebnerBasis_iff_minimal
Theorem
151
MonomialOrder.IsGroebnerBasis.IsReduced.congr_simp
Theorem
152
MonomialOrder.IsGroebnerBasis.IsMinimal.congr_simp
Lemma
153
isGroebnerBasis_minimal
Lemma
154
isGroebnerBasis_monomial
Lemma
155
isGroebnerBasis_monomial_minimal
Lemma
159
span_image_leadingTerm
Lemma
165
MonomialOrder.IsGroebnerBasis.IsReduced.of_subsingleton
Lemma
166
MonomialOrder.IsGroebnerBasis.IsMinimal.of_subsingleton
Lemma
167
isReduced_monomial
Lemma
168
image_leadingTerm_eq_image_monomial_one
Lemma
169
isReduced_leadingTerm
Lemma
170
isGroebnerBasis_of_isMinimal_leadingTerm
Lemma
173
isMinimal_iff_monic_and_minimal_degree_and_injOn_leadingTerm
Lemma
174
degree_image_eq_setOf_minimal
Lemma
175
degree_image_eq_of_isMinimal
Lemma
176
isMinimal_of_isMinimal_leadingTerm
Lemma
177
leadingCoeff_add_of_lt_right
Lemma
179
degree_le_mul_left
Lemma
180
withBotDegree_eq_of_isRemainder
Lemma
181
degree_eq_of_isRemainder
Lemma
182
leadingTerm_eq_of_isRemainder
Lemma
183
isGroebnerBasis_image_isRemainder
Lemma
184
isReduced_image_isRemainder_of_IsMinimal
Lemma
185
exists_of_isGroebnerBasis
Lemma
186
exists_of_isGroebnerBasis₀
Lemma
187
exists_of_isGroebnerBasis’
Theorem
188
uniqueExists_of_isGroebnerBasis
Theorem
189
uniqueExists_of_isGroebnerBasis₀
Lemma
191
isGroebnerBasis_minimalFor
Lemma
192
isReduced_minimalFor
Theorem
193
isReduced_iff_minimalFor
Lemma
194
union_mem_of_mem
Lemma
195
biUnion_mem_of_mem
Lemma
196
sUnion_mem_of_mem
Lemma
197
iUnion_mem_of_mem
Theorem
198
subset_limsup
Theorem
199
isReduced_liminf
Theorem
200
isReduced_liminf_nat