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

The Banach open mapping theorem #897

Closed
wants to merge 2 commits into from
Closed

The Banach open mapping theorem #897

wants to merge 2 commits into from

Conversation

sgouezel
Copy link
Collaborator

@sgouezel sgouezel commented Apr 7, 2019

TO CONTRIBUTORS:

Make sure you have:

  • reviewed and applied the coding style: coding, naming
  • make sure definitions and lemmas are put in the right files
  • make sure definitions and lemmas are not redundant

@sgouezel sgouezel requested a review from a team as a code owner April 7, 2019 12:32
@sgouezel sgouezel mentioned this pull request Apr 8, 2019
Merged
@robertylewis
Copy link
Member

Just for the record, this is superseded by #900 and is open for testing purposes.

avigad
avigad approved these changes Apr 16, 2019
View reviewed changes
Copy link
Collaborator

@avigad avigad left a comment

Choose a reason for hiding this comment

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

Looks great to me.

@avigad avigad added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) labels Apr 16, 2019
@avigad avigad removed their assignment Apr 16, 2019
@sgouezel sgouezel closed this Apr 25, 2019
@sgouezel sgouezel deleted the open_mapping branch December 2, 2019 10:36
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Reviewers

@avigad avigad avigad approved these changes

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
3 participants
@sgouezel @robertylewis @avigad