Skip to content

[Merged by Bors] - feat: port Topology.Algebra.Order.UpperLower#2503

Closed
mo271 wants to merge 5 commits intomasterfrom
port/Topology.Algebra.Order.UpperLower
Closed

[Merged by Bors] - feat: port Topology.Algebra.Order.UpperLower#2503
mo271 wants to merge 5 commits intomasterfrom
port/Topology.Algebra.Order.UpperLower

Conversation

@mo271
Copy link
Copy Markdown
Collaborator

@mo271 mo271 commented Feb 26, 2023 •
edited by github-actions bot
Loading

mo271 added 4 commits February 26, 2023 14:27
@mo271
feat: port Topology.Algebra.Order.UpperLower
88abdc7
@mo271
Initial file copy from mathport
9b367b2
@mo271
automated fixes
3e29cc8 
Mathbin -> Mathlib

fix certain import statements

move "by" to end of line

add import to Mathlib.lean
@mo271
first pass
95ea007
@mo271 mo271 added the mathlib-port This is a port of a theory file from mathlib. label Feb 26, 2023
@mo271
Copy link
Copy Markdown
Collaborator Author

mo271 commented Feb 26, 2023

comm_semigroup.is_central_scalar recently changed (got to_additive) and apparently group_theory/group_action/opposite needs some syncing or something...

@mo271 mo271 added the WIP Work in progress label Feb 26, 2023
@mo271
Copy link
Copy Markdown
Collaborator Author

mo271 commented Feb 26, 2023

already in progress, I see: #2344

@mo271 mo271 added blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) and removed WIP Work in progress labels Feb 26, 2023
@kim-em kim-em added blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) and removed blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) labels Feb 26, 2023
@kim-em
Copy link
Copy Markdown
Contributor

kim-em commented Mar 1, 2023

This PR/issue depends on:

@kim-em kim-em added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Mar 1, 2023
@kim-em kim-em removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Mar 2, 2023
jcommelin
jcommelin approved these changes Mar 2, 2023
View reviewed changes
Copy link
Copy Markdown
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

@kim-em kim-em added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Mar 2, 2023
bors bot pushed a commit that referenced this pull request Mar 2, 2023
@mo271
feat: port Topology.Algebra.Order.UpperLower (#2503)
4f884ff 
- [x] depends on: #2344



Co-authored-by: Moritz Firsching <firsching@google.com>
@bors
Copy link
Copy Markdown

bors bot commented Mar 2, 2023

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat: port Topology.Algebra.Order.UpperLower [Merged by Bors] - feat: port Topology.Algebra.Order.UpperLower Mar 2, 2023
@bors bors bot closed this Mar 2, 2023
@bors bors bot deleted the port/Topology.Algebra.Order.UpperLower branch March 2, 2023 08:11
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@jcommelin jcommelin jcommelin approved these changes

Assignees

No one assigned

Labels

mathlib-port This is a port of a theory file from mathlib. ready-to-merge This PR has been sent to bors.

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@mo271 @kim-em @jcommelin