mathlib4 feat(RingTheory/MvPolynomial/Groebner): add Gröbner basis

This PR adds some definitions and theorems of Gröbner basis theory.

Definitions:

MonomialOrder.IsRemainder
MonomialOrder.IsGroebnerBasis

Main theorems:

MonomialOrder.remainder_eq_zero_iff_mem_ideal_of_isGroebnerBasis: Given a remainder of a polynomial on division by a Gröbner basis of an ideal, the remainder is 0 if and only if the polynomial is in the ideal.
MonomialOrder.isGroebnerBasis_iff_subset_ideal_and_isRemainder_zero: A finite 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 finite set.
MonomialOrder.existsUnique_isRemainder_of_isGroebnerBasis: Remainder of any polynomial on division by a Gröbner basis exists and is unique.
MonomialOrder.ideal_eq_span_of_isGroebnerBasis: Gröbner basis of any ideal spans the ideal.
MonomialOrder.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.

The previous Mathlib/RingTheory/MvPolynomial/Groebner.lean is moved to Mathlib/RingTheory/MvPolynomial/Groebner/Division.lean, and used by Mathlib/RingTheory/MvPolynomial/Groebner/Remainder.lean for the proof of remainder's existence.

The PR is upstreamized from https://github.com/WuProver/groebner_proj.

Co-authored-by: Hao Shen [email protected]

CC @tsuki8

TODO:

[x] clean up some proofs
[x] split the file
[x] squeeze Non-terminal simps
[x] add comments to explain the proof of Buchberger Criterion.

Dependencies:

[x] depends on: #26039

S-polynomial and other lemmas in other files are split from this PR, leaving only changes of Mathlib/RingTheory/MvPolynomial/Groebner{.lean,/*.lean} in this PR. The following are PRs split from this PR.

[x] depends on: #32336
[x] depends on: #32344
[x] depends on: #32780
[x] depends on: #32787
[x] depends on: #32788
[x] depends on: #32801
[x] depends on: #32876
[x] depends on: #32877

Sep 01 '25 08:09 Hagb

PR summary 94e04f1e44

Import changes exceeding 2%

%	File
+2.25%	`Mathlib.RingTheory.MvPolynomial.Groebner`

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.RingTheory.MvPolynomial.Groebner	1020	1043	+23 (+2.25%)

Import changes for all files

Files	Import difference
`Mathlib.Combinatorics.Nullstellensatz`	22
`Mathlib.RingTheory.MvPolynomial.Groebner`	23
`Mathlib.RingTheory.MvPolynomial.Groebner.Division` (new file)	1020
`Mathlib.RingTheory.MvPolynomial.Groebner.Remainder` (new file)	1025

Declarations diff

+ IsGroebnerBasis + IsRemainder + existsUnique_isRemainder_of_isGroebnerBasis + existsUnique_isRemainder_of_isGroebnerBasis₀ + exists_degree_le_degree_of_isRemainder_zero + exists_degree_le_degree_of_isRemainder_zero' + exists_degree_le_degree_of_isRemainder_zero₀ + exists_isGroebnerBasis_finite + exists_isRemainder + exists_isRemainder' + exists_isRemainder₀ + ideal_eq_span_of_isGroebnerBasis + isGroebnerBasis_iff_ideal_eq_span_and_isGroebnerBasis_span + isGroebnerBasis_iff_isRemainder_sPolynomial_zero + isGroebnerBasis_iff_isRemainder_sPolynomial_zero' + isGroebnerBasis_iff_span_eq_and_degree_le + isGroebnerBasis_iff_subset_ideal_and_isRemainder_zero + isGroebnerBasis_iff_subset_ideal_and_isRemainder_zero' + isGroebnerBasis_iff_subset_ideal_and_isRemainder_zero₀ + isGroebnerBasis_insert_zero + isGroebnerBasis_sdiff_singleton_zero + isGroebnerBasis_self + isRemainder_def' + isRemainder_def'' + isRemainder_def'₁ + isRemainder_finset + isRemainder_finset₁ + isRemainder_finset₁' + isRemainder_finset₁₀ + isRemainder_insert_zero_iff_isRemainder + isRemainder_range + isRemainder_sdiff_singleton_zero_iff_isRemainder + isRemainder_zero + isRemainder_zero' + isRemainder_zero_iff_mem_ideal_of_isGroebnerBasis + isRemainder_zero_iff_mem_ideal_of_isGroebnerBasis' + isRemainder_zero_iff_mem_ideal_of_isGroebnerBasis₀ + isRemainder_zero₀ + mem_ideal_iff_of_isRemainder + mem_ideal_of_isRemainder_of_mem_ideal + monomial_notMem_span_leadingTerm + monomial_notMem_span_leadingTerm_of_isRemainder + monomial_notMem_span_leadingTerm_of_isRemainder₀ + remainder_eq_zero_iff_mem_ideal_of_isGroebnerBasis + remainder_eq_zero_iff_mem_ideal_of_isGroebnerBasis' + remainder_eq_zero_iff_mem_ideal_of_isGroebnerBasis₀ + span_leadingTerm_eq_span_monomial_of_isGroebnerBasis + span_leadingTerm_eq_span_monomial_of_isGroebnerBasis₀ + sub_mem_ideal_of_isRemainder_of_subset_ideal + sub_monomial_notMem_span_leadingTerm_of_isRemainder + term_notMem_span_leadingTerm_of_isRemainder + term_notMem_span_leadingTerm_of_isRemainder' + term_notMem_span_leadingTerm_of_isRemainder₀

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).