-
Notifications
You must be signed in to change notification settings - Fork 247
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.
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
[Merged by Bors] - refactor: new definition of eigenvectorUnitary
#11363
Conversation
…but it isn't that bad.
Want to remove mul_vec and vec_mul lemmas and then address issues with #align commands
…nk_eq_rank_diagonal broke.
by using tactic mode.
…ral" alignment with previously existing lemmas.
Replaced Hermitian conjugate with star. Co-authored-by: Jireh Loreaux <loreaujy@gmail.com>
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I think it's getting close. You should probably switch from WIP
to awaiting-review
though.
Jireh's suggestion, more explicit eigenvectorBasis Co-authored-by: Jireh Loreaux <loreaujy@gmail.com>
…com/leanprover-community/mathlib4 into jbannon/Spectrum.eigenvectorUnitary
I've had a lot of input in this, so it would be good to get a second set of eyes. maintainer merge |
🚀 Pull request has been placed on the maintainer queue by j-loreaux. |
eigenvectorUnitary
Definitely 👍
…On Fri, May 3, 2024, 12:52 PM Jireh Loreaux ***@***.***> wrote:
I've had a lot of input in this, so it would be good to get a second set
of eyes.
maintainer merge
—
Reply to this email directly, view it on GitHub
<#11363 (comment)>,
or unsubscribe
<https://github.com/notifications/unsubscribe-auth/AOJJJTURPHUYLLPOTCS4ZVTZAO6EBAVCNFSM6AAAAABEVA72J6VHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDAOJTGM4TCNBUG4>
.
You are receiving this because you authored the thread.Message ID:
***@***.***>
|
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thanks 🎉
bors merge
This file contains the spectral theorem for Hermitian matrices and nearby relevant theorems. We rewrote the file, recasting the natural eigenvector basis matrix as a unitary called `eigenvectorUnitary`, and removed a lot of defeq abuse that the original file contained, considerably simplifying things. Co-authored-by: JonBannon <59937998+JonBannon@users.noreply.github.com>
Pull request successfully merged into master. Build succeeded: |
eigenvectorUnitary
eigenvectorUnitary
This file contains the spectral theorem for Hermitian matrices and nearby relevant theorems. We rewrote the file, recasting the natural eigenvector basis matrix as a unitary called `eigenvectorUnitary`, and removed a lot of defeq abuse that the original file contained, considerably simplifying things. Co-authored-by: JonBannon <59937998+JonBannon@users.noreply.github.com>
This file contains the spectral theorem for Hermitian matrices and nearby relevant theorems. We rewrote the file, recasting the natural eigenvector basis matrix as a unitary called `eigenvectorUnitary`, and removed a lot of defeq abuse that the original file contained, considerably simplifying things. Co-authored-by: JonBannon <59937998+JonBannon@users.noreply.github.com>
This file contains the spectral theorem for Hermitian matrices and nearby relevant theorems. We rewrote the file, recasting the natural eigenvector basis matrix as a unitary called
eigenvectorUnitary
, and removed a lot of defeq abuse that the original file contained, considerably simplifying things.rank_mul_eq_left_of_isUnit_det
into an effectivesimp
lemma #12244