Skip to content

[Merged by Bors] - feat(RingTheory/MvPolynomial/Groebner): division algorithm wrt monomial orders#19454

Closed
AntoineChambert-Loir wants to merge 15 commits intomasterfrom
ACL/Groebner-da
Closed

[Merged by Bors] - feat(RingTheory/MvPolynomial/Groebner): division algorithm wrt monomial orders#19454
AntoineChambert-Loir wants to merge 15 commits intomasterfrom
ACL/Groebner-da

Conversation

@AntoineChambert-Loir
Copy link
Copy Markdown
Collaborator

@AntoineChambert-Loir AntoineChambert-Loir commented Nov 25, 2024

Formalize the division algorithm with respect to a monomial order

This is part of an ongoing work to formalize Groebner theory.
For the moment, only the lexicographic order is present in mathlib, but
subsequent PRs will introduce the homogeneous lexicographic order and the homogeneous
reverse lexicographic order.

Open in Gitpod

@github-actions
Copy link
Copy Markdown

github-actions bot commented Nov 25, 2024 •
edited
Loading

PR summary 9351e29a98

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference
Mathlib.RingTheory.MvPolynomial.MonomialOrder (new file) 1102
Mathlib.RingTheory.MvPolynomial.Groebner (new file) 1103

Declarations diff

+ coeff_degree_eq_zero_iff
+ coeff_degree_ne_zero_iff
+ coeff_eq_zero_of_lt
+ coeff_mul_of_degree_add
+ degree
+ degree_C
+ degree_add_le
+ degree_add_of_lt
+ degree_add_of_ne
+ degree_eq_zero_iff_totalDegree_eq_zero
+ degree_le_iff
+ degree_lt_iff
+ degree_monomial
+ degree_monomial_le
+ degree_mul
+ degree_mul_le
+ degree_mul_of_isRegular_left
+ degree_mul_of_isRegular_right
+ degree_mul_of_nonzero_mul
+ degree_neg
+ degree_reduce_lt
+ degree_smul
+ degree_smul_le
+ degree_sub_LTerm_le
+ degree_sub_LTerm_lt
+ degree_sub_le
+ degree_sub_of_lt
+ degree_zero
+ div
+ div_set
+ eq_C_of_degree_eq_zero
+ lCoeff
+ lCoeff_add_of_lt
+ lCoeff_eq_zero_iff
+ lCoeff_is_unit_iff
+ lCoeff_monomial
+ lCoeff_mul
+ lCoeff_mul_of_isRegular_left
+ lCoeff_mul_of_isRegular_right
+ lCoeff_ne_zero_iff
+ lCoeff_sub_of_lt
+ lCoeff_zero
+ le_degree
+ reduce
+ subLTerm
+ sup_mem_of_nonempty

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).

@mathlib4-dependent-issues-bot mathlib4-dependent-issues-bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Nov 25, 2024
@AntoineChambert-Loir AntoineChambert-Loir mentioned this pull request Nov 25, 2024
Closed
@AntoineChambert-Loir AntoineChambert-Loir mentioned this pull request Nov 25, 2024
Closed
6 tasks
@AntoineChambert-Loir AntoineChambert-Loir changed the title feat(Mathlib/RingTheory/MvPolynomial/Groebner): division algorithm wrt monomial orders feat(RingTheory/MvPolynomial/Groebner): division algorithm wrt monomial orders Nov 25, 2024
@mathlib4-dependent-issues-bot mathlib4-dependent-issues-bot removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Nov 25, 2024
@mathlib4-dependent-issues-bot
Copy link
Copy Markdown
Collaborator

mathlib4-dependent-issues-bot commented Nov 25, 2024

This PR/issue depends on:

@leanprover-community-bot-assistant leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Nov 25, 2024
@leanprover-community-bot-assistant leanprover-community-bot-assistant removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Nov 25, 2024
@jcommelin jcommelin self-assigned this Nov 28, 2024
@jcommelin
Copy link
Copy Markdown
Member

jcommelin commented Dec 4, 2024

This looks great! Thanks for doing this 🎉

bors merge

@ghost ghost added the ready-to-merge This PR has been sent to bors. label Dec 4, 2024
mathlib-bors bot pushed a commit that referenced this pull request Dec 4, 2024
@AntoineChambert-Loir
feat(RingTheory/MvPolynomial/Groebner): division algorithm wrt monomi…
ea51583 
…al orders (#19454)

Formalize the division algorithm with respect to a monomial order

This is part of an ongoing work to formalize Groebner theory.
For the moment, only the lexicographic order is present in mathlib, but 
subsequent PRs will introduce the homogeneous lexicographic order and the homogeneous
reverse lexicographic order.
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Dec 4, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(RingTheory/MvPolynomial/Groebner): division algorithm wrt monomial orders [Merged by Bors] - feat(RingTheory/MvPolynomial/Groebner): division algorithm wrt monomial orders Dec 4, 2024
@mathlib-bors mathlib-bors bot closed this Dec 4, 2024
@mathlib-bors mathlib-bors bot deleted the ACL/Groebner-da branch December 4, 2024 06:32
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

@jcommelin jcommelin

Labels

ready-to-merge This PR has been sent to bors.

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

4 participants

@AntoineChambert-Loir @mathlib4-dependent-issues-bot @jcommelin @leanprover-community-bot-assistant