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(algebra/module/linear_map): Move elementwise structure from linear_algebra/basic #9331
Conversation
…linear_algebra/basic This helps reduce the size of linear_algebra/basic, and by virtue of being a smaller file makes it easier to spot typeclasses which can be relaxed. In particular, `linear_map.endomorphism_ring` now requires only `semiring R` not `ring R`.
I wouldn't normally do this, but is there any chance this could wait until after #9272 is merged? It looks like it won't be too long now, and having to keep up with major refactors in |
I've split out the non-major-refactor part of this PR as #9335 |
Thanks a lot! |
…_map-arithmetic # Conflicts: # src/algebra/module/linear_map.lean # src/linear_algebra/basic.lean
🎉 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 merge |
…linear_algebra/basic (#9331) This helps reduce the size of linear_algebra/basic, and by virtue of being a smaller file makes it easier to spot typeclasses which can be relaxed. As an example, `linear_map.endomorphism_ring` now requires only `semiring R` not `ring R`. Having instances available as early as possible is generally good, as otherwise it is hard to even state things elsewhere.
Build failed (retrying...): |
…linear_algebra/basic (#9331) This helps reduce the size of linear_algebra/basic, and by virtue of being a smaller file makes it easier to spot typeclasses which can be relaxed. As an example, `linear_map.endomorphism_ring` now requires only `semiring R` not `ring R`. Having instances available as early as possible is generally good, as otherwise it is hard to even state things elsewhere.
Pull request successfully merged into master. Build succeeded: |
This helps reduce the size of linear_algebra/basic, and by virtue of being a smaller file makes it easier to spot typeclasses which can be relaxed.
As an example,
linear_map.endomorphism_ring
now requires onlysemiring R
notring R
.Having instances available as early as possible is generally good, as otherwise it is hard to even state things elsewhere.
linear_map.neg_comp
, generalizelinear_map.{sub,smul}_comp
#9335linear_map.add_comm_group
to semilinear maps #9402