Skip to content

[Merged by Bors] - feat: bundled version of Cardinal.ord_eq#36928

Closed
vihdzp wants to merge 13 commits intoleanprover-community:masterfrom
vihdzp:bundled
Closed

[Merged by Bors] - feat: bundled version of Cardinal.ord_eq#36928
vihdzp wants to merge 13 commits intoleanprover-community:masterfrom
vihdzp:bundled

Conversation

@vihdzp
Copy link
Copy Markdown
Collaborator

@vihdzp vihdzp commented Mar 21, 2026

For any type, there exists a (bundled) well-ordering whose order type is ord #α.

Open in Gitpod

@vihdzp vihdzp added the t-set-theory Set theory label Mar 21, 2026
@github-actions
Copy link
Copy Markdown

github-actions bot commented Mar 21, 2026 •
edited
Loading

PR summary e960b84129

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ exists_ord_eq_type_lt
+ mk_Iio_lt
+ mk_Iio_toType_ord_lt

You can run this locally as follows 
## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>

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

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

No changes to technical debt.

You can run this locally as

./scripts/reporting/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).

@vihdzp vihdzp mentioned this pull request Mar 21, 2026
Open
3 tasks
@vihdzp vihdzp requested a review from YaelDillies March 28, 2026 08:32
YaelDillies
YaelDillies approved these changes Mar 28, 2026
View reviewed changes
Copy link
Copy Markdown
Contributor

@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 delegate

@github-actions
Copy link
Copy Markdown

github-actions bot commented Mar 28, 2026

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

pull_request_review, wf_run

@mathlib-triage mathlib-triage bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Mar 28, 2026
@vihdzp vihdzp mentioned this pull request Mar 29, 2026
Closed
1 task
@riccardobrasca
Copy link
Copy Markdown
Member

riccardobrasca commented Mar 30, 2026

Thanks!

bors merge

@mathlib-triage mathlib-triage 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 Mar 30, 2026
mathlib-bors bot pushed a commit that referenced this pull request Mar 30, 2026
@vihdzp
feat: bundled version of Cardinal.ord_eq (#36928)
e1df007 
For any type, there exists a (bundled) well-ordering whose order type is `ord #α`.
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Mar 30, 2026

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat: bundled version of Cardinal.ord_eq [Merged by Bors] - feat: bundled version of Cardinal.ord_eq Mar 30, 2026
@mathlib-bors mathlib-bors bot closed this Mar 30, 2026
mathlib-bors bot pushed a commit that referenced this pull request Mar 30, 2026
@vihdzp
refactor: rename Cardinal.ord_eq → Cardinal.exists_ord_eq (#37330)
975f9e8 
As suggested in #36928.
aditya-ramabadran pushed a commit to aditya-ramabadran/mathlib4 that referenced this pull request Apr 1, 2026
@vihdzp @aditya-ramabadran
feat: bundled version of Cardinal.ord_eq (leanprover-community#36928)
fdaf62f 
For any type, there exists a (bundled) well-ordering whose order type is `ord #α`.
aditya-ramabadran pushed a commit to aditya-ramabadran/mathlib4 that referenced this pull request Apr 1, 2026
@vihdzp @aditya-ramabadran
refactor: rename Cardinal.ord_eq → Cardinal.exists_ord_eq (leanpr…
23e40df 
…over-community#37330)

As suggested in leanprover-community#36928.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@YaelDillies YaelDillies YaelDillies approved these changes

Assignees

No one assigned

Labels

ready-to-merge This PR has been sent to bors. t-set-theory Set theory

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@vihdzp @riccardobrasca @YaelDillies