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

[Merged by Bors] - feat(order/upper_lower): ×ˢ notation for upper/lower sets#17746

Closed
YaelDillies wants to merge 3 commits intomasterfrom
upper_lower_prod_notation
Closed

[Merged by Bors] - feat(order/upper_lower): ×ˢ notation for upper/lower sets#17746
YaelDillies wants to merge 3 commits intomasterfrom
upper_lower_prod_notation

Conversation

@YaelDillies
Copy link
Copy Markdown
Collaborator

Introduce ×ˢ notation for upper_set.prod and lower_set.prod.


Open in Gitpod

@YaelDillies YaelDillies added awaiting-review The author would like community review of the PR easy < 20s of review time. See the lifecycle page for guidelines. t-order Order hierarchy labels Nov 28, 2022
Copy link
Copy Markdown
Member

@eric-wieser eric-wieser left a comment

Choose a reason for hiding this comment

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

Can you add to the module docstring to mention the notation?

bors d+

@bors
Copy link
Copy Markdown

bors bot commented Nov 28, 2022

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

@leanprover-community-bot-assistant leanprover-community-bot-assistant added delegated The PR author may merge after reviewing final suggestions. and removed awaiting-review The author would like community review of the PR labels Nov 28, 2022
@YaelDillies
Copy link
Copy Markdown
Collaborator Author

bors merge

bors bot pushed a commit that referenced this pull request Nov 29, 2022
Introduce `×ˢ` notation for `upper_set.prod`  and `lower_set.prod`.
@bors
Copy link
Copy Markdown

bors bot commented Nov 29, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(order/upper_lower): ×ˢ notation for upper/lower sets [Merged by Bors] - feat(order/upper_lower): ×ˢ notation for upper/lower sets Nov 29, 2022
@bors bors bot closed this Nov 29, 2022
@bors bors bot deleted the upper_lower_prod_notation branch November 29, 2022 05:27
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.

Labels

delegated The PR author may merge after reviewing final suggestions. easy < 20s of review time. See the lifecycle page for guidelines. t-order Order hierarchy

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants