[Merged by Bors] - feat(Data/Finsupp/MonomialOrder/DegLex): homogeneous lexicographic order by AntoineChambert-Loir · Pull Request #19455 · leanprover-community/mathlib4

AntoineChambert-Loir · 2024-11-25T09:59:31Z

Definition of the homogeneous lexicographic order

This is part of an ongoing work on basic of Gröbner theory.
A subsequent PR will add the homogeneous reverse lexicographic order.

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

github-actions · 2024-11-25T10:00:33Z

PR summary 233c68d4a6

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
`Mathlib.Data.Finsupp.MonomialOrder.DegLex` (new file)	882

Declarations diff

+ DegLex.exists_iff
+ DegLex.forall_iff
+ DegLex.rec
+ Lex.single_antitone
+ Lex.single_le_iff
+ Lex.single_lt_iff
+ Lex.single_strictAnti
+ degLex
+ degLex_def
+ degLex_le_iff
+ degLex_lt_iff
+ degLex_single_le_iff
+ degLex_single_lt_iff
+ degree_add
+ degree_single
+ instance :
+ instance : LinearOrder (DegLex (α →₀ ℕ))
+ instance : OrderedCancelAddCommMonoid (DegLex (α →₀ ℕ))
+ instance [AddCommMonoid α] :
+ instance [LT α] : LT (DegLex (α →₀ ℕ))
+ isStrictOrder
+ le_iff
+ lt_def
+ lt_iff
+ monotone_degree
+ ofDegLex
+ ofDegLex_add
+ ofDegLex_inj
+ ofDegLex_injective
+ ofDegLex_symm_eq
+ ofDegLex_toDegLex
+ orderBot
+ single_antitone
+ single_le_iff
+ single_lt_iff
+ single_strictAnti
+ toDegLex
+ toDegLex_add
+ toDegLex_inj
+ toDegLex_injective
+ toDegLex_ofDegLex
+ toDegLex_symm_eq
+ wellFounded
+ wellFoundedLT
++ DegLex

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 · 2024-11-25T13:14:00Z

This PR/issue depends on:

~~[Merged by Bors] - feat(Data/Finsupp/MonomialOrder): monomial orders #19453~~
By Dependent Issues (🤖). Happy coding!

Mathlib/Data/Finsupp/MonomialOrder/DegLex.lean

joelriou · 2024-11-26T19:53:34Z

I have only very minor suggestions, otherwise it looks good to me.

…ommunity/mathlib4 into ACL/Groebner-deglex

Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>

…ommunity/mathlib4 into ACL/Groebner-deglex

Mathlib/Data/Finsupp/MonomialOrder/DegLex.lean

AntoineChambert-Loir · 2024-11-29T22:28:53Z

Yet another question: this file requires RingTheory/MvPolynomial/MonomialOrder. So probably it better fits that hierarchy than the Data/Finsupp one. What do you think?

Mathlib/Data/Finsupp/MonomialOrder/DegLex.lean

joelriou · 2024-12-03T17:03:11Z

Yet another question: this file requires RingTheory/MvPolynomial/MonomialOrder. So probably it better fits that hierarchy than the Data/Finsupp one. What do you think?

It seems we do not have RingTheory/MvPolynomial/MonomialOrder?! Anyway, I think it is fine in Data.Finsupp.

Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>

joelriou · 2024-12-04T18:37:03Z

Thanks!

bors merge

…der (#19455) Definition of the homogeneous lexicographic order This is part of an ongoing work on basic of Gröbner theory. A subsequent PR will add the homogeneous reverse lexicographic order.

mathlib-bors · 2024-12-04T18:59:05Z

Pull request successfully merged into master.

Build succeeded:

AntoineChambert-Loir added 3 commits November 25, 2024 10:41

initial commit

d1861ea

remove useless instances (linter alert)

0cccee7

initial commit

b483dfb

github-actions bot added the t-data Data (lists, quotients, numbers, etc) label Nov 25, 2024

AntoineChambert-Loir mentioned this pull request Nov 25, 2024

feat(Data/Finsupp/MonomialOrder/DegRevLex): homogeneous reverse lexicographic order #19456

Open

2 tasks

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 added 4 commits November 25, 2024 11:26

add two import

a6fbe9b

add finsupp/weight lemmas

b3d9a6c

add finsupp/Lex lemmas

03a67c7

add references

2d8270c

This was referenced Nov 25, 2024

feat (Mathlib/RingTheory/MvPolynomial/Groebner) : monomial orders and division #16584

Closed

[Merged by Bors] - feat: Lemmas for some monomial orders #16177

Closed

AntoineChambert-Loir added t-algebraic-geometry Algebraic geometry t-order Order theory labels Nov 25, 2024

AntoineChambert-Loir changed the title ~~feat(Mathlib/Data/Finsupp/MonomialOrder/DegLex): homogeneous lexicographic order~~ feat(Data/Finsupp/MonomialOrder/DegLex): homogeneous lexicographic order Nov 25, 2024

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

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

Merge branch 'master' into ACL/Groebner-deglex

bd03624

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

joelriou reviewed Nov 26, 2024

View reviewed changes

Mathlib/Data/Finsupp/MonomialOrder/DegLex.lean Outdated Show resolved Hide resolved

joelriou reviewed Nov 26, 2024

View reviewed changes

Mathlib/Data/Finsupp/MonomialOrder/DegLex.lean Outdated Show resolved Hide resolved

joelriou reviewed Nov 26, 2024

View reviewed changes

Mathlib/Data/Finsupp/MonomialOrder/DegLex.lean Outdated Show resolved Hide resolved

joelriou reviewed Nov 26, 2024

View reviewed changes

Mathlib/Data/Finsupp/MonomialOrder/DegLex.lean Outdated Show resolved Hide resolved

joelriou reviewed Nov 26, 2024

View reviewed changes

Mathlib/Data/Finsupp/MonomialOrder/DegLex.lean Outdated Show resolved Hide resolved

joelriou reviewed Nov 26, 2024

View reviewed changes

Mathlib/Data/Finsupp/MonomialOrder/DegLex.lean Outdated Show resolved Hide resolved

joelriou added the awaiting-author A reviewer has asked the author a question or requested changes. label Nov 26, 2024

Merge branch 'ACL/Groebner-deglex' of https://github.com/leanprover-c…

2b22e9d

…ommunity/mathlib4 into ACL/Groebner-deglex

AntoineChambert-Loir and others added 3 commits November 27, 2024 05:52

Apply suggestions from code review

35dc6cf

Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>

Merge branch 'ACL/Groebner-deglex' of https://github.com/leanprover-c…

192fb57

…ommunity/mathlib4 into ACL/Groebner-deglex

apply Joël's suggestions, add namespaces, make an example section

4a610ea

AntoineChambert-Loir commented Nov 27, 2024

View reviewed changes

Mathlib/Data/Finsupp/MonomialOrder/DegLex.lean Outdated Show resolved Hide resolved

AntoineChambert-Loir removed the awaiting-author A reviewer has asked the author a question or requested changes. label Nov 27, 2024

joelriou added the awaiting-author A reviewer has asked the author a question or requested changes. label Nov 27, 2024

AntoineChambert-Loir removed the awaiting-author A reviewer has asked the author a question or requested changes. label Nov 29, 2024

mv example section at the end

d8f17dd

joelriou reviewed Dec 3, 2024

View reviewed changes

Mathlib/Data/Finsupp/MonomialOrder/DegLex.lean Outdated Show resolved Hide resolved

joelriou reviewed Dec 3, 2024

View reviewed changes

Mathlib/Data/Finsupp/MonomialOrder/DegLex.lean Show resolved Hide resolved

joelriou reviewed Dec 3, 2024

View reviewed changes

Mathlib/Data/Finsupp/MonomialOrder/DegLex.lean Outdated Show resolved Hide resolved

joelriou added the awaiting-author A reviewer has asked the author a question or requested changes. label Dec 3, 2024

AntoineChambert-Loir and others added 3 commits December 4, 2024 11:23

Update Mathlib/Data/Finsupp/MonomialOrder/DegLex.lean

30fbb44

Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>

Apply suggestions from code review

93b2a73

Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>

whereify definition of structure

233c68d

AntoineChambert-Loir removed the awaiting-author A reviewer has asked the author a question or requested changes. label Dec 4, 2024

ghost added the ready-to-merge This PR has been sent to bors. label Dec 4, 2024

mathlib-bors bot changed the title ~~feat(Data/Finsupp/MonomialOrder/DegLex): homogeneous lexicographic order~~ [Merged by Bors] - feat(Data/Finsupp/MonomialOrder/DegLex): homogeneous lexicographic order Dec 4, 2024

mathlib-bors bot closed this Dec 4, 2024

mathlib-bors bot deleted the ACL/Groebner-deglex branch December 4, 2024 19:00

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat(Data/Finsupp/MonomialOrder/DegLex): homogeneous lexicographic order#19455

[Merged by Bors] - feat(Data/Finsupp/MonomialOrder/DegLex): homogeneous lexicographic order#19455
AntoineChambert-Loir wants to merge 16 commits intomasterfrom
ACL/Groebner-deglex

AntoineChambert-Loir commented Nov 25, 2024 •

edited by joelriou

Loading

Uh oh!

github-actions bot commented Nov 25, 2024 •

edited

Loading

Declarations diff

Uh oh!

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

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

joelriou commented Nov 26, 2024

Uh oh!

Uh oh!

AntoineChambert-Loir commented Nov 29, 2024

Uh oh!

Uh oh!

Uh oh!

Uh oh!

joelriou commented Dec 3, 2024

Uh oh!

joelriou commented Dec 4, 2024

Uh oh!

mathlib-bors bot commented Dec 4, 2024

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

Conversation

AntoineChambert-Loir commented Nov 25, 2024 • edited by joelriou Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Nov 25, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 233c68d4a6

Import changes for modified files

Declarations diff

Uh oh!

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

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

joelriou commented Nov 26, 2024

Uh oh!

Uh oh!

AntoineChambert-Loir commented Nov 29, 2024

Uh oh!

Uh oh!

Uh oh!

Uh oh!

joelriou commented Dec 3, 2024

Uh oh!

joelriou commented Dec 4, 2024

Uh oh!

mathlib-bors bot commented Dec 4, 2024

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

AntoineChambert-Loir commented Nov 25, 2024 •

edited by joelriou

Loading

github-actions bot commented Nov 25, 2024 •

edited

Loading