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] - Matrix.dotProduct inequalities #9652

Closed
wants to merge 3 commits into from
Closed

[Merged by Bors] - Matrix.dotProduct inequalities #9652

wants to merge 3 commits into from

Conversation

madvorak
Copy link
Collaborator

Open in Gitpod

@madvorak madvorak mentioned this pull request Jan 12, 2024
Open
1 task
dupuisf
dupuisf reviewed Jan 15, 2024
View reviewed changes
Copy link
Contributor

@dupuisf dupuisf 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 r+

@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Jan 15, 2024
mathlib-bors bot pushed a commit that referenced this pull request Jan 15, 2024
@madvorak
Matrix.dotProduct inequalities (#9652)
18cc8db
@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented Jan 15, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title Matrix.dotProduct inequalities [Merged by Bors] - Matrix.dotProduct inequalities Jan 15, 2024
@mathlib-bors mathlib-bors bot closed this Jan 15, 2024
@mathlib-bors mathlib-bors bot deleted the dp-ineq branch January 15, 2024 15:17
linesthatinterlace pushed a commit that referenced this pull request Jan 16, 2024
@madvorak @linesthatinterlace
Matrix.dotProduct inequalities (#9652)
c9dcb79
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@dupuisf dupuisf dupuisf left review comments

Assignees
No one assigned
Labels
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
@madvorak @dupuisf @leanprover-community-mathlib4-bot