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(Data/Matrix/Basic): 0 ≤ 1 #12911

Closed
wants to merge 3 commits into from
Closed

[Merged by Bors] - feat(Data/Matrix/Basic): 0 ≤ 1 #12911

wants to merge 3 commits into from

Conversation

madvorak
Copy link
Collaborator

Open in Gitpod

madvorak and others added 2 commits May 15, 2024 09:31
@madvorak @Rida-Hamadani
Update Mathlib/Data/Matrix/Basic.lean
4de5930 
Co-authored-by: Rida Hamadani <106540880+Rida-Hamadani@users.noreply.github.com>
@madvorak
cosmetic improvement
c35a835
@riccardobrasca
Copy link
Member

Does it make sense to add the ZeroLEOneClass instance to matrix ring?

@madvorak
Copy link
Collaborator Author

Does it make sense to add the ZeroLEOneClass instance to matrix ring?

I don't know. Would it allow me to say 0 ≤ 1 also for matrices, not just for their elements and their rows?

@riccardobrasca
Copy link
Member

Let's try and bench the result, it those are OK it cannot hurt.

@jcommelin
Copy link
Member

Is there an ordering defined on matrices?

@madvorak
Copy link
Collaborator Author

Is there an ordering defined on matrices?

Not to my knowledge.
If we want to define it, perhaps a separate PR?

@riccardobrasca
Copy link
Member

riccardobrasca commented May 16, 2024 •
edited
Loading

I just realized that I misread the statement. Forget my comment.

jcommelin
jcommelin reviewed May 16, 2024
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-mathlib4-bot leanprover-community-mathlib4-bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels May 16, 2024
mathlib-bors bot pushed a commit that referenced this pull request May 16, 2024
@madvorak
feat(Data/Matrix/Basic): 0 ≤ 1 (#12911)
ac523ae
@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented May 16, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(Data/Matrix/Basic): 0 ≤ 1 [Merged by Bors] - feat(Data/Matrix/Basic): 0 ≤ 1 May 16, 2024
@mathlib-bors mathlib-bors bot closed this May 16, 2024
@mathlib-bors mathlib-bors bot deleted the matrix0le1 branch May 16, 2024 15:07
callesonne pushed a commit that referenced this pull request May 16, 2024
@madvorak @callesonne
feat(Data/Matrix/Basic): 0 ≤ 1 (#12911)
f18af6a
grunweg pushed a commit that referenced this pull request May 17, 2024
@madvorak @grunweg
feat(Data/Matrix/Basic): 0 ≤ 1 (#12911)
27563ad
@madvorak madvorak restored the matrix0le1 branch August 22, 2024 11:15
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@jcommelin jcommelin jcommelin left review comments

@Rida-Hamadani Rida-Hamadani Rida-Hamadani 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.
5 participants
@madvorak @riccardobrasca @jcommelin @Rida-Hamadani @leanprover-community-mathlib4-bot