-
Notifications
You must be signed in to change notification settings - Fork 259
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: generalize scalars in Algebra.lsmul #6209
Conversation
…ra instance This also moves some lemmas about `IsUnit (_ : Module.End R M)` to an earlier file as they are nothing to do with `Algebra`.
(note the CI failure will be resolved once the dependent PR is merged) |
This PR/issue depends on: |
Thanks! bors merge |
This generalizes from `Algebra.lsmul R M : A →ₐ[R] Module.End R M` to `Algebra.lsmul R S M : A →ₐ[R] Module.End S M`. This generalization was previously not possible because `Module.End S M` was not an `R`-algebra. Notably this now allows things like `Algebra.lsmul R A A : Aᵐᵒᵖ →ₐ[R] Module.End A A` (right multiplication). This doesn't bother attempting to generalize uses in downstream files, as most of them probably do not need the generality. Instead, we just replace `Algebra.lsmul R` with `Algebra.lsmul R R`.
Pull request successfully merged into master. Build succeeded! The publicly hosted instance of bors-ng is deprecated and will go away soon. If you want to self-host your own instance, instructions are here. If you want to switch to GitHub's built-in merge queue, visit their help page. |
This generalizes from `Algebra.lsmul R M : A →ₐ[R] Module.End R M` to `Algebra.lsmul R S M : A →ₐ[R] Module.End S M`. This generalization was previously not possible because `Module.End S M` was not an `R`-algebra. Notably this now allows things like `Algebra.lsmul R A A : Aᵐᵒᵖ →ₐ[R] Module.End A A` (right multiplication). This doesn't bother attempting to generalize uses in downstream files, as most of them probably do not need the generality. Instead, we just replace `Algebra.lsmul R` with `Algebra.lsmul R R`.
This generalizes from `Algebra.lsmul R M : A →ₐ[R] Module.End R M` to `Algebra.lsmul R S M : A →ₐ[R] Module.End S M`. This generalization was previously not possible because `Module.End S M` was not an `R`-algebra. Notably this now allows things like `Algebra.lsmul R A A : Aᵐᵒᵖ →ₐ[R] Module.End A A` (right multiplication). This doesn't bother attempting to generalize uses in downstream files, as most of them probably do not need the generality. Instead, we just replace `Algebra.lsmul R` with `Algebra.lsmul R R`.
This generalizes from `Algebra.lsmul R M : A →ₐ[R] Module.End R M` to `Algebra.lsmul R S M : A →ₐ[R] Module.End S M`. This generalization was previously not possible because `Module.End S M` was not an `R`-algebra. Notably this now allows things like `Algebra.lsmul R A A : Aᵐᵒᵖ →ₐ[R] Module.End A A` (right multiplication). This doesn't bother attempting to generalize uses in downstream files, as most of them probably do not need the generality. Instead, we just replace `Algebra.lsmul R` with `Algebra.lsmul R R`.
This generalizes from
Algebra.lsmul R M : A →ₐ[R] Module.End R M
toAlgebra.lsmul R S M : A →ₐ[R] Module.End S M
.This generalization was previously not possible because
Module.End S M
was not anR
-algebra.Notably this now allows things like
Algebra.lsmul R A A : Aᵐᵒᵖ →ₐ[R] Module.End A A
(right multiplication).This doesn't bother attempting to generalize uses in downstream files, as most of them probably do not need the generality.
Instead, we just replace
Algebra.lsmul R
withAlgebra.lsmul R R
.