Skip to content

[Merged by Bors] - feat(Data/Finsupp/MonomialOrder): monomial orders#19453

Closed
AntoineChambert-Loir wants to merge 4 commits intomasterfrom
ACL/Groebner-mo
Closed

[Merged by Bors] - feat(Data/Finsupp/MonomialOrder): monomial orders#19453
AntoineChambert-Loir wants to merge 4 commits intomasterfrom
ACL/Groebner-mo

Conversation

@AntoineChambert-Loir
Copy link
Copy Markdown
Collaborator

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

Definition of monomial orders, with the example of the lexicographic ordering

This is the starting point of implementation of the beginnings of Gröbner theory.
3 subsequent PRs will address:

  • division algorithm
  • example of the homogeneous lexicographic ordering
  • example of the homogeneous reverse lexicographic ordering

These various orderings (and other ones…) may look exotic but are actually used in algebraic geometry.

Open in Gitpod

@AntoineChambert-Loir AntoineChambert-Loir added t-algebraic-geometry Algebraic geometry t-algebra Algebra (groups, rings, fields, etc) t-order Order theory labels Nov 25, 2024
@github-actions
Copy link
Copy Markdown

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

PR summary 72a011cafd

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference
Mathlib.Data.Finsupp.MonomialOrder (new file) 786

Declarations diff

+ Finsupp.lex_le_iff
+ Finsupp.lex_lt_iff
+ MonomialOrder
+ MonomialOrder.lex
+ MonomialOrder.lex_le_iff
+ MonomialOrder.lex_lt_iff
+ bot_eq_zero
+ eq_zero_iff
+ instance {α N : Type*} [LinearOrder α] [OrderedCancelAddCommMonoid N] :
+ le_add_right
+ orderBot
+ toSyn_strictMono

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

@AntoineChambert-Loir AntoineChambert-Loir mentioned this pull request Nov 25, 2024
Closed
1 task
This was referenced Nov 25, 2024
Closed
Open
@AntoineChambert-Loir AntoineChambert-Loir mentioned this pull request Nov 25, 2024
Closed
@jcommelin jcommelin changed the title feature(Mathlib/Data/Finsupp/MonomialOrder): monomial orders feat(Mathlib/Data/Finsupp/MonomialOrder): monomial orders Nov 25, 2024
@jcommelin jcommelin changed the title feat(Mathlib/Data/Finsupp/MonomialOrder): monomial orders feat(Data/Finsupp/MonomialOrder): monomial orders Nov 25, 2024
jcommelin
jcommelin reviewed Nov 25, 2024
View reviewed changes
@AntoineChambert-Loir AntoineChambert-Loir mentioned this pull request Nov 25, 2024
Closed
6 tasks
AntoineChambert-Loir
AntoineChambert-Loir commented Nov 25, 2024
View reviewed changes
@AntoineChambert-Loir @jcommelin
Apply suggestions from code review
72a011c 
Co-authored-by: Johan Commelin <johan@commelin.net>
@jcommelin
Copy link
Copy Markdown
Member

jcommelin commented Nov 25, 2024

Thanks 🎉

If CI passes, please remove the label awaiting-CI and merge this yourself, by adding a comment bors r+.

bors d+

@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Nov 25, 2024

✌️ AntoineChambert-Loir can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@jcommelin jcommelin added the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Nov 25, 2024
@ghost ghost added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Nov 25, 2024
@github-actions github-actions bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Nov 25, 2024
@AntoineChambert-Loir
Copy link
Copy Markdown
Collaborator Author

AntoineChambert-Loir commented Nov 25, 2024

bors r+

mathlib-bors bot pushed a commit that referenced this pull request Nov 25, 2024
@AntoineChambert-Loir
feat(Data/Finsupp/MonomialOrder): monomial orders (#19453)
7f28d7f 
Definition of monomial orders, with the example of the lexicographic ordering

This is the starting point of implementation of the beginnings of Gröbner theory.
3 subsequent PRs will address:
- division algorithm
- example of the homogeneous lexicographic ordering
- example of the homogeneous reverse lexicographic ordering

These various orderings (and other ones…) may look exotic but are actually used in algebraic geometry.
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Nov 25, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(Data/Finsupp/MonomialOrder): monomial orders [Merged by Bors] - feat(Data/Finsupp/MonomialOrder): monomial orders Nov 25, 2024
@mathlib-bors mathlib-bors bot closed this Nov 25, 2024
@mathlib-bors mathlib-bors bot deleted the ACL/Groebner-mo branch November 25, 2024 13:12
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@jcommelin jcommelin jcommelin left review comments

Assignees

No one assigned

Labels

delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). t-algebra Algebra (groups, rings, fields, etc) t-algebraic-geometry Algebraic geometry t-order Order theory

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@AntoineChambert-Loir @jcommelin