- Boxes
- definitions
- Ellipses
- theorems and lemmas
- Blue border
- the statement of this result is ready to be formalized; all prerequisites are done
- Orange border
- the statement of this result is not ready to be formalized; the blueprint needs more work
- Blue background
- the proof of this result is ready to be formalized; all prerequisites are done
- Green border
- the statement of this result is formalized
- Green background
- the proof of this result is formalized
- Dark green background
- the proof of this result and all its ancestors are formalized
- Dark green border
- this is in Mathlib
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.
A subset G of an ideal I is said to be a Gröbner basis if:
G is contained in I (i.e., all polynomials in G belong to the ideal I).
The ideal generated by the leading terms of all polynomials in I is equal to the ideal generated by the leading terms of the polynomials in G.
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.
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.
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.
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.
Given a multivariate polynomial f and a set B of multivariate polynomials over R. A polynomial r is called a remainder of f on division by B with respect to a monomial order m, if there exists g : B →₀ R[X] and a polynomial r s.t.
Finite linear combination: f = ∑ (g(b) * b) + r;
Degree condition: For eacho b ∈ B, the degree (with bot) of g(b) * b ≤ the degree (with bot) of f w.r.t. m;
Remainder irreducibility: No term of r is divisible by the leading monomial of any non-zero b ∈ B.
The definition of remainder makes sense when R is a communitive ring and any polynomial in B either has an invertible leading coefficient or is 0. See the implementation note for the formalization unaligned with the informal definition when not in this case.
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.
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.
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.