Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[Merged by Bors] - feat(analysis/matrix): define the frobenius norm on matrices #13497

Closed
wants to merge 17 commits into from
Closed

[Merged by Bors] - feat(analysis/matrix): define the frobenius norm on matrices #13497

wants to merge 17 commits into from

Conversation

eric-wieser
Copy link
Member

@eric-wieser eric-wieser commented Apr 18, 2022 •
edited by github-actions bot
Loading

@eric-wieser
chore(analysis/normed_space/finite_dimension): golf a proof
f12e181 
These `letI`s just made this proof convoluted, the instances were not needed.
Similarly, the `classical` was the cause of the need for the `congr`.
@eric-wieser
chore(analysis): lemmas about nnorm
321d06d
@eric-wieser
wip
d9530b6
@eric-wieser
wip
403f25b
@eric-wieser
fix
0fa629b
@eric-wieser eric-wieser added awaiting-author A reviewer has asked the author a question or requested changes awaiting-CI The author would like to see what CI has to say before doing more work. labels Apr 18, 2022
@leanprover-community-bot-assistant leanprover-community-bot-assistant added the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Apr 18, 2022
@leanprover-community-bot-assistant leanprover-community-bot-assistant added blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. merge-conflict Please `git merge origin/master` then a bot will remove this label. and removed blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. labels Apr 18, 2022
@leanprover-community-bot-assistant leanprover-community-bot-assistant removed the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Apr 19, 2022
@eric-wieser eric-wieser added this to In Progress in Matrix exponential Apr 20, 2022
@leanprover-community-bot-assistant leanprover-community-bot-assistant added the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Apr 21, 2022
@leanprover-community-bot-assistant leanprover-community-bot-assistant removed the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Apr 21, 2022
@leanprover-community-bot-assistant leanprover-community-bot-assistant added the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Apr 22, 2022
@github-actions github-actions bot removed the awaiting-CI The author would like to see what CI has to say before doing more work. label Apr 22, 2022
@eric-wieser eric-wieser 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 Apr 22, 2022
@leanprover-community-bot-assistant leanprover-community-bot-assistant removed the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Apr 29, 2022
@leanprover-community-bot-assistant
Copy link
Collaborator

This PR/issue depends on:

@leanprover-community-bot-assistant leanprover-community-bot-assistant added the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Apr 29, 2022
@leanprover-community-bot-assistant leanprover-community-bot-assistant removed the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Apr 29, 2022
jcommelin
jcommelin approved these changes May 2, 2022
View reviewed changes
Copy link
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

@leanprover-community-bot-assistant leanprover-community-bot-assistant 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 awaiting-review The author would like community review of the PR labels May 2, 2022
bors bot pushed a commit that referenced this pull request May 2, 2022
@eric-wieser
feat(analysis/matrix): define the frobenius norm on matrices (#13497)
1e38549
@bors
Copy link

bors bot commented May 2, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(analysis/matrix): define the frobenius norm on matrices [Merged by Bors] - feat(analysis/matrix): define the frobenius norm on matrices May 2, 2022
@bors bors bot closed this May 2, 2022
Matrix exponential automation moved this from In Progress to Done May 2, 2022
@bors bors bot deleted the eric-wieser/matrix-frobenius branch May 2, 2022 07:50
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
ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.)
Projects
No open projects
Matrix exponential
  
Done
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
3 participants
@eric-wieser @leanprover-community-bot-assistant @jcommelin