-
Notifications
You must be signed in to change notification settings - Fork 298
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/sesquilinear_form): preliminary results for nondegeneracy #12269
Conversation
… mcdoll/bilinear_refactor
I don't see why the build fails, |
Just labelling |
Oh, I am sorry. I did not expect the linter to complain. |
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.
You might want to split all the small changes to prerequisite files into a separate PR. They look ready for merging to me. Then the reviews can focus on the new material.
what is the best way to do the split in git? I would just cut and paste all the nondegenerate stuff into a new PR, but maybe there is a better option |
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
…generacy (#12269) Several lemmas needed to define nondegenerate bilinear forms and show that the canonical pairing of the algebraic dual is nondegenerate. Add domain restriction of bilinear maps in the second component and in both compenents. Some type-class generalizations for symmetric, alternating, and reflexive sesquilinear forms.
Pull request successfully merged into master. Build succeeded: |
…generacy (#12269) Several lemmas needed to define nondegenerate bilinear forms and show that the canonical pairing of the algebraic dual is nondegenerate. Add domain restriction of bilinear maps in the second component and in both compenents. Some type-class generalizations for symmetric, alternating, and reflexive sesquilinear forms.
… new file. (#18468) This cuts the import path. The copyright comes from #12269. I chose not to just move these lemmas to `linear_algebra/basis` as this file is already huge. The moved lemmas are now stated slightly more generally (`comm_semiring` rather than `comm_ring`), which seems to have been an accident in the original file as no proofs had to change.
Several lemmas needed to define nondegenerate bilinear forms and show that the canonical pairing of the algebraic dual is nondegenerate.
Add domain restriction of bilinear maps in the second component and in both compenents.
Some type-class generalizations for symmetric, alternating, and reflexive sesquilinear forms.