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/basic, group_theory/quotient_group, algebra/lie/quotient): ext lemmas for morphisms out of quotients #8641
Conversation
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.
Nice work, the proofs clean up noticeably!
@ocfnash, could you check the Lie algebra parts?
(in case you missed it @Vierkantor, Oliver commented at #8641 (comment) already) |
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 r+ |
…uotient): ext lemmas for morphisms out of quotients (#8641) This allows `ext` to see through quotients by subobjects of a type `A`, and apply ext lemmas specific to `A`.
Build failed (retrying...): |
…uotient): ext lemmas for morphisms out of quotients (#8641) This allows `ext` to see through quotients by subobjects of a type `A`, and apply ext lemmas specific to `A`.
Pull request successfully merged into master. Build succeeded: |
This allows
ext
to see through quotients by subobjects of a typeA
, and apply ext lemmas specific toA
.