Skip to content
This repository has been archived by the owner on Jul 24, 2024. It is now read-only.

feat(order/flag): Order isomorphisms act on flags #18754

Closed
wants to merge 3 commits into from
Closed

feat(order/flag): Order isomorphisms act on flags #18754

wants to merge 3 commits into from

Conversation

YaelDillies
Copy link
Collaborator

and inherit the grading of their ambient order.

Open in Gitpod

@YaelDillies YaelDillies added awaiting-review The author would like community review of the PR t-order Order hierarchy modifies-synchronized-file This PR touches a files that has already been ported to mathlib4, and may need a synchronization PR. labels Apr 7, 2023
eric-wieser
eric-wieser reviewed Apr 7, 2023
View reviewed changes
src/order/chain.lean Outdated Show resolved Hide resolved
vihdzp
vihdzp reviewed Apr 8, 2023
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 all looks good to me, but not familiar enough with these files to give explicit approval.

I really should get back to my abstract polytope development.

@YaelDillies
Copy link
Collaborator Author

Inspiration was taken from there, in fact! I cleaned up what I could and this I could polish enough to make a PR.

eric-wieser
eric-wieser reviewed Jul 13, 2023
View reviewed changes
src/order/flag.lean Outdated Show resolved Hide resolved
eric-wieser
eric-wieser reviewed Jul 13, 2023
View reviewed changes
src/order/flag.lean Outdated Show resolved Hide resolved
@eric-wieser eric-wieser added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Jul 13, 2023
@YaelDillies YaelDillies added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Jul 14, 2023
@kim-em kim-em added the too-late This PR was ready too late for inclusion in mathlib3 label Jul 16, 2023
@YaelDillies
Copy link
Collaborator Author

Why is this marked too-late? It compiles except for the fact that bibtool fails to install, unrelatingly to the PR.

@YaelDillies YaelDillies added not-too-late This PR was ready at the point mathlib3 was frozen: we will try to merge it and port it to mathlib4 and removed too-late This PR was ready too late for inclusion in mathlib3 labels Jul 17, 2023
@YaelDillies
Copy link
Collaborator Author

Ported to LeanCamCombi

@YaelDillies YaelDillies deleted the grade_flag branch November 18, 2023 10:54
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Reviewers

@vihdzp vihdzp vihdzp left review comments

@eric-wieser eric-wieser eric-wieser left review comments

Assignees
No one assigned
Labels
awaiting-review The author would like community review of the PR modifies-synchronized-file This PR touches a files that has already been ported to mathlib4, and may need a synchronization PR. not-too-late This PR was ready at the point mathlib3 was frozen: we will try to merge it and port it to mathlib4 t-order Order hierarchy
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
4 participants
@YaelDillies @eric-wieser @vihdzp @kim-em