-
Notifications
You must be signed in to change notification settings - Fork 297
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] - feat(linear_algebra/matrix/adjugate): det_adjugate and adjugate_adjugate #9991
Conversation
e031b7f
to
5c3379f
Compare
efbb066
to
d0b802f
Compare
[comm_semiring R] [comm_semiring S] [algebra R S] (A : matrix m m S) : | ||
(mv_polynomial.aeval $ λ p : m × m, A p.1 p.2).map_matrix (mv_polynomial_X m m R) = A := | ||
mv_polynomial_X_map_eval₂ _ A | ||
|
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.
Could you please add some lemmas saying that the evaluation maps are surjective (and/or have partial inverses)?
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.
Can you be precise about what you consider to be the evaluation map, and in which argument you want to state surjectivity?
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.
Sorry, I was confused. mv_polynomial R ℤ
has a surjective ring hom to R
, by evaluation. I thought this was a variant on that, but it is of course slightly different.
Co-authored-by: Johan Commelin <johan@commelin.net>
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
[comm_semiring R] [comm_semiring S] [algebra R S] (A : matrix m m S) : | ||
(mv_polynomial.aeval $ λ p : m × m, A p.1 p.2).map_matrix (mv_polynomial_X m m R) = A := | ||
mv_polynomial_X_map_eval₂ _ A | ||
|
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.
Sorry, I was confused. mv_polynomial R ℤ
has a surjective ring hom to R
, by evaluation. I thought this was a variant on that, but it is of course slightly different.
…ate (#9991) This also adds `matrix.mv_polynomial_X`
Build failed (retrying...): |
…ate (#9991) This also adds `matrix.mv_polynomial_X`
Build failed (retrying...): |
…ate (#9991) This also adds `matrix.mv_polynomial_X`
Pull request successfully merged into master. Build succeeded: |
…ate (#9991) This also adds `matrix.mv_polynomial_X`
This also adds
matrix.mv_polynomial_X