-
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/direct_sum): submodule_is_internal_iff_independent_and_supr_eq_top
#9214
Conversation
Also golf some uses of `quotient.lift_on` to use `quotient.map`.
…uotient.lift_on`" This reverts commit 7f136ef.
complete_lattice.independent_iff_dfinsupp_lsum_ker
submodule_is_internal_iff_independent_and_supr_eq_top
…p-injective-independent
🎉 Great news! Looks like all the dependencies have been resolved:
💡 To add or remove a dependency please update this issue/PR description. Brought to you by Dependent Issues (:robot: ). Happy coding! |
bors d+ |
✌️ eric-wieser can now approve this pull request. To approve and merge a pull request, simply reply with |
Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Johan Commelin <johan@commelin.net>
Thanks 🎉 bors merge |
I'm a little puzzled by bors here. This PR has the label "awaiting-CI" but bors did not reject it. As far as I know bors uses the configuration from the master branch, which indeed contains: Line 7 in c33407a
|
Perhaps bors won't reject it until it hits the top of the queue? |
Ah, I misremembered! From the docs
|
…nt_and_supr_eq_top` (#9214) This shows that a grade decomposition into submodules is bijective iff and only iff the submodules are independent and span the whole module. The key proofs are: * `complete_lattice.independent_of_dfinsupp_lsum_injective` * `complete_lattice.independent.dfinsupp_lsum_injective` Everything else is just glue. This replaces parts of #8246, and uses what is probably a similar proof strategy, but without unfolding down to finsets. Unlike the proof there, this requires only `add_comm_monoid` for the `complete_lattice.independent_of_dfinsupp_lsum_injective` direction of the proof. I was not able to find a proof of `complete_lattice.independent.dfinsupp_lsum_injective` with the same weak assumptions, as it is not true! A counter-example is included, Co-authored-by: Hanting Zhang <hantingzhang03@gmail.com>
Pull request successfully merged into master. Build succeeded: |
submodule_is_internal_iff_independent_and_supr_eq_top
submodule_is_internal_iff_independent_and_supr_eq_top
This shows that a grade decomposition into submodules is bijective iff and only iff the submodules are independent and span the whole module.
The key proofs are:
complete_lattice.independent_of_dfinsupp_lsum_injective
complete_lattice.independent.dfinsupp_lsum_injective
Everything else is just glue.
This replaces parts of #8246, and uses what is probably a similar proof strategy, but without unfolding down to finsets.
Unlike the proof there, this requires only
add_comm_monoid
for thecomplete_lattice.independent_of_dfinsupp_lsum_injective
direction of the proof. I was not able to find a proof ofcomplete_lattice.independent.dfinsupp_lsum_injective
with the same weak assumptions, as it is not true! A counter-example is included,Co-authored-by: Hanting Zhang hantingzhang03@gmail.com
filter_ne_eq_erase
#9182