Skip to content

[Merged by Bors] - feat(Order): OrderIso involving Prod and Lex #33663

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Closed
YanYablonovskiy wants to merge 5 commits into from
Closed

[Merged by Bors] - feat(Order): OrderIso involving Prod and Lex #33663

YanYablonovskiy wants to merge 5 commits into from

Conversation

@YanYablonovskiy
Copy link
Contributor

@YanYablonovskiy YanYablonovskiy commented Jan 6, 2026

Adding some results that are needed for order types, in particular the monoids on them(see #33420).

Open in Gitpod

@github-actions github-actions bot added the new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! label Jan 6, 2026
@github-actions
Copy link

github-actions bot commented Jan 6, 2026 •
edited
Loading

PR summary b79634a5c1

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ emptySumLex
+ emptySumLex_apply_inr
+ ofIsEmpty
+ prodAssoc
+ prodLexAssoc
+ prodLexCongr
+ sumLexEmpty
+ sumLexEmpty_apply_inl
+ sumLexProdLexDistrib

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

@YaelDillies YaelDillies changed the title Feat: Prod and Lex results for OrderIso feat(Order): OrderIso involving Prod and Lex Jan 6, 2026
vihdzp
vihdzp reviewed Jan 6, 2026
View reviewed changes
Copy link
Collaborator

@vihdzp vihdzp left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This largely looks good, you should un-draft this.

@vihdzp vihdzp added the t-order Order theory label Jan 6, 2026
@YanYablonovskiy
Squashed commit of the following:
5811e1d 
commit d51b84d
Author: YanYablonovskiy <[email protected]>
Date:   Tue Jan 6 20:13:26 2026 +1100

    OrderIso prod lemmas adjustment

commit 4c41035
Merge: b88c734 15f6691
Author: Yan Yablonovskiy <[email protected]>
Date:   Tue Jan 6 20:04:32 2026 +1100

    Merge branch 'master' into master

commit b88c734
Author: YanYablonovskiy <[email protected]>
Date:   Tue Jan 6 19:33:15 2026 +1100

    Changes from review

commit 8252446
Author: Yan Yablonovskiy <[email protected]>
Date:   Tue Jan 6 16:00:09 2026 +1100

    Apply suggestions from code review

    Co-authored-by: Violeta Hernández Palacios <[email protected]>

commit 8ac8458
Author: YanYablonovskiy <[email protected]>
Date:   Tue Jan 6 01:11:04 2026 +1100

    Change mathlib imports from `OrderType`

    `OrderType.lean` no longer exists

commit f353fe8
Merge: 30bd77d 959c852
Author: Yan Yablonovskiy <[email protected]>
Date:   Mon Jan 5 23:17:21 2026 +1100

    Merge branch 'leanprover-community:master' into master

commit 30bd77d
Author: YanYablonovskiy <[email protected]>
Date:   Mon Jan 5 21:49:57 2026 +1100

    Refactor as per suggestions, back to `LinOrd`

commit f8cd844
Merge: f04b327 a57b343
Author: YanYablonovskiy <[email protected]>
Date:   Mon Jan 5 21:49:30 2026 +1100

    Merge branch 'master' of https://github.com/YanYablonovskiy/mathlib4_Order-types-Issue28278

commit f04b327
Author: YanYablonovskiy <[email protected]>
Date:   Mon Jan 5 11:36:50 2026 +1100

    Apply suggestions

commit a57b343
Merge: 5937b50 8c8bf56
Author: Yan Yablonovskiy <[email protected]>
Date:   Mon Jan 5 11:30:56 2026 +1100

    Merge branch 'leanprover-community:master' into master

commit 5937b50
Merge: 07abc73 2330302
Author: YanYablonovskiy <[email protected]>
Date:   Mon Jan 5 10:21:08 2026 +1100

    Merge branch 'master' of https://github.com/YanYablonovskiy/mathlib4_Order-types-Issue28278

commit 2330302
Author: Yan Yablonovskiy <[email protected]>
Date:   Mon Jan 5 10:20:45 2026 +1100

    Apply suggestions from code review

    Co-authored-by: Yaël Dillies <[email protected]>
    Co-authored-by: Violeta Hernández Palacios <[email protected]>

commit 07abc73
Author: YanYablonovskiy <[email protected]>
Date:   Mon Jan 5 00:44:02 2026 +1100

    Fix recommended_spellings

commit b25cb4c
Author: YanYablonovskiy <[email protected]>
Date:   Mon Jan 5 00:37:52 2026 +1100

    Add doc-string and some more typos

commit 067b8cd
Author: YanYablonovskiy <[email protected]>
Date:   Mon Jan 5 00:31:32 2026 +1100

    Minor typos

commit 4b5a837
Author: YanYablonovskiy <[email protected]>
Date:   Sun Jan 4 22:26:24 2026 +1100

    Finish conversation review suggestions

commit 5429c1b
Author: Yan Yablonovskiy <[email protected]>
Date:   Fri Jan 2 23:31:29 2026 +1100

    Apply suggestions from code review

    [skip ci]

    Co-authored-by: Yaël Dillies <[email protected]>
    Co-authored-by: Violeta Hernández Palacios <[email protected]>

commit 630f0ea
Author: YanYablonovskiy <[email protected]>
Date:   Fri Jan 2 23:14:37 2026 +1100

    Style fix

commit bf5166d
Author: YanYablonovskiy <[email protected]>
Date:   Fri Jan 2 22:58:10 2026 +1100

    Fix module error

commit 2f0a005
Merge: 44753fe 519f454
Author: Yan Yablonovskiy <[email protected]>
Date:   Fri Jan 2 20:11:02 2026 +1100

    Merge branch 'leanprover-community:master' into master

commit 44753fe
Author: YanYablonovskiy <[email protected]>
Date:   Fri Jan 2 19:42:27 2026 +1100

    Bump

commit 43b7d68
Author: YanYablonovskiy <[email protected]>
Date:   Fri Jan 2 19:18:34 2026 +1100

    Clean up imports, get rid of sorries, and address some comments

commit f888e2b
Author: YanYablonovskiy <[email protected]>
Date:   Thu Jan 1 22:12:33 2026 +1100

    Update OrderType.lean

    Add copyright
    [skip actions]

commit 9848662
Author: YanYablonovskiy <[email protected]>
Date:   Thu Jan 1 21:56:01 2026 +1100

    Update OrderType.lean

commit b8acc2e
Author: Yan Yablonovskiy <[email protected]>
Date:   Thu Jan 1 20:15:25 2026 +1100

    Apply suggestions from code review

    Co-authored-by: Violeta Hernández Palacios <[email protected]>
    Co-authored-by: Yaël Dillies <[email protected]>

commit a5e62be
Merge: 6aa39b3 de80207
Author: YanYablonovskiy <[email protected]>
Date:   Wed Dec 31 16:34:44 2025 +1100

    Merge branch 'master' of https://github.com/YanYablonovskiy/mathlib4_Order-types-Issue28278

commit 6aa39b3
Author: YanYablonovskiy <[email protected]>
Date:   Wed Dec 31 16:34:33 2025 +1100

    Update OrderType.lean

commit de80207
Merge: 669a1d3 6dc6d70
Author: Yan Yablonovskiy <[email protected]>
Date:   Wed Dec 31 16:34:24 2025 +1100

    Merge branch 'leanprover-community:master' into master

commit 669a1d3
Merge: a90d529 6371049
Author: Yan Yablonovskiy <[email protected]>
Date:   Mon Dec 29 10:38:08 2025 +1100

    Merge branch 'leanprover-community:master' into master

commit a90d529
Merge: 24bb5b0 cc5691d
Author: Yan Yablonovskiy <[email protected]>
Date:   Mon Dec 22 13:06:26 2025 +1100

    Merge branch 'leanprover-community:master' into master

commit 24bb5b0
Merge: 4985680 5334b1e
Author: Yan Yablonovskiy <[email protected]>
Date:   Wed Nov 26 18:44:18 2025 +1100

    Merge branch 'leanprover-community:master' into master

commit 4985680
Merge: 711df94 3f87ea8
Author: Yan Yablonovskiy <[email protected]>
Date:   Sun Nov 23 12:48:18 2025 +1100

    Merge branch 'leanprover-community:master' into master

commit 711df94
Merge: 6534400 b3cf7a0
Author: Yan Yablonovskiy <[email protected]>
Date:   Sat Nov 22 13:48:50 2025 +1100

    Merge branch 'leanprover-community:master' into master

commit 6534400
Merge: bb1a642 56c98a5
Author: Yan Yablonovskiy <[email protected]>
Date:   Thu Nov 20 18:46:50 2025 +1100

    Merge branch 'leanprover-community:master' into master

commit bb1a642
Author: YanYablonovskiy <[email protected]>
Date:   Mon Oct 20 21:27:21 2025 +1100

    Update OrderType.lean

commit f427a91
Author: YanYablonovskiy <[email protected]>
Date:   Mon Oct 20 18:25:16 2025 +1100

    Update OrderType.lean

commit f6c13a0
Author: YanYablonovskiy <[email protected]>
Date:   Mon Oct 20 17:59:56 2025 +1100

    Update OrderType.lean

commit 78e4c9a
Author: YanYablonovskiy <[email protected]>
Date:   Mon Oct 20 16:29:31 2025 +1100

    Update OrderType.lean

commit e827b3c
Author: YanYablonovskiy <[email protected]>
Date:   Sat Oct 18 00:41:45 2025 +1100

    Update OrderType.lean

commit f5d5427
Author: YanYablonovskiy <[email protected]>
Date:   Sat Oct 18 00:23:18 2025 +1100

    Update OrderType.lean

commit 871acb9
Author: YanYablonovskiy <[email protected]>
Date:   Fri Oct 17 22:32:05 2025 +1100

    Update OrderType.lean

commit 803ced6
Author: YanYablonovskiy <[email protected]>
Date:   Fri Oct 17 20:45:37 2025 +1100

    Update OrderType.lean

commit 2883e90
Author: YanYablonovskiy <[email protected]>
Date:   Thu Oct 16 23:04:21 2025 +1100

    Update OrderType.lean

commit 971c382
Author: Yan Yablonovskiy <[email protected]>
Date:   Thu Oct 16 23:02:18 2025 +1100

    Update OrderType.lean

commit 3db4465
Author: Yan Yablonovskiy <[email protected]>
Date:   Thu Oct 16 23:01:46 2025 +1100

    Update OrderType.lean

commit 3e7c325
Author: YanYablonovskiy <[email protected]>
Date:   Thu Oct 16 22:59:05 2025 +1100

    Update OrderType.lean

commit ce284fa
Author: Yan Yablonovskiy <[email protected]>
Date:   Tue Oct 14 20:26:41 2025 +1100

    Update OrderType.lean

commit e0e79c8
Author: YanYablonovskiy <[email protected]>
Date:   Tue Oct 14 19:02:32 2025 +1100

    Create OrderTypes file with definition and some generalisation from Ordinal

commit e78fa58
Merge: aa54d18 3aa3aca
Author: Yan Yablonovskiy <[email protected]>
Date:   Tue Oct 14 19:02:04 2025 +1100

    Merge branch 'leanprover-community:master' into master

commit aa54d18
Merge: 3742a3b efcc0aa
Author: Yan Yablonovskiy <[email protected]>
Date:   Sun Sep 21 15:21:45 2025 +1000

    Merge branch 'leanprover-community:master' into master

commit 3742a3b
Author: YanYablonovskiy <[email protected]>
Date:   Sat Sep 20 22:28:23 2025 +1000

    Create OrderTypes_basic.lean
vihdzp
vihdzp reviewed Jan 7, 2026
View reviewed changes
@YanYablonovskiy YanYablonovskiy marked this pull request as ready for review January 7, 2026 06:15
vihdzp
vihdzp approved these changes Jan 7, 2026
View reviewed changes
Copy link
Collaborator

@vihdzp vihdzp left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM modulo minor remarks

@YanYablonovskiy
Code review suggestions
148988f 
And generalizing results about empty lexicographic sum orders to just less-than (as opposed to `Preorder`).
@YanYablonovskiy
Fix name
9e7e23c
@vihdzp vihdzp requested a review from YaelDillies January 7, 2026 07:01
YaelDillies
YaelDillies approved these changes Jan 7, 2026
View reviewed changes
Copy link
Collaborator

@YaelDillies YaelDillies left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks! 🚀

maintainer merge

@github-actions
Copy link

github-actions bot commented Jan 7, 2026

🚀 Pull request has been placed on the maintainer queue by YaelDillies.

@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Jan 7, 2026
jcommelin
jcommelin reviewed Jan 7, 2026
View reviewed changes
Copy link
Member

@jcommelin jcommelin left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks 🎉

bors merge

@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added ready-to-merge This PR has been sent to bors. and removed maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. labels Jan 7, 2026
mathlib-bors bot pushed a commit that referenced this pull request Jan 7, 2026
@YanYablonovskiy
feat(Order): OrderIso involving Prod and Lex (#33663)
94fe2a2 
Adding some results that are needed for order types, in particular the monoids on them(see #33420).

Co-authored-by: YanYablonovskiy <[email protected]>
@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented Jan 7, 2026

This PR was included in a batch that was canceled, it will be automatically retried

mathlib-bors bot pushed a commit that referenced this pull request Jan 7, 2026
@YanYablonovskiy
feat(Order): OrderIso involving Prod and Lex (#33663)
84dc72c 
Adding some results that are needed for order types, in particular the monoids on them(see #33420).

Co-authored-by: YanYablonovskiy <[email protected]>
@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented Jan 7, 2026

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(Order): OrderIso involving Prod and Lex [Merged by Bors] - feat(Order): OrderIso involving Prod and Lex Jan 7, 2026
@mathlib-bors mathlib-bors bot closed this Jan 7, 2026
@YanYablonovskiy YanYablonovskiy mentioned this pull request Jan 16, 2026
Open
2 tasks
@github-actions github-actions bot mentioned this pull request Jan 16, 2026
Open
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

@YaelDillies YaelDillies YaelDillies approved these changes

+1 more reviewer

@vihdzp vihdzp vihdzp approved these changes

Reviewers whose approvals may not affect merge requirements

Assignees

No one assigned

Labels

new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! ready-to-merge This PR has been sent to bors. t-order Order theory

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

5 participants

@YanYablonovskiy @jcommelin @YaelDillies @vihdzp @leanprover-community-mathlib4-bot