[Merged by Bors] - feat: base change for Lie modules #8546
Conversation
ocfnash
commented
Nov 21, 2023
ocfnash
commented
ocfnash
added
awaiting-review
|
|
||
| namespace LieAlgebra | ||
|
|
||
| namespace ExtendScalars | ||
|
|
||
| variable [CommRing R] [CommRing A] [Algebra R A] [LieRing L] [LieAlgebra R L] | ||
| [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] | ||
|
|
||
| /-- The Lie bracket on the extension of a Lie algebra `L` over `R` by an algebra `A` over `R`. -/ |
There was a problem hiding this comment.
Can you update this docstring to mention M? I don't know the non-lean way to write the terminology, but persumably you want to talk about the lie module bracket or similar.
There was a problem hiding this comment.
bors r-
It looks like you didn't touch this docstring? Given the 👍 I assume that wasn't deliberate? If it was, feel free to re-merge.
There was a problem hiding this comment.
Argh, apologies I missed this and confused myself into thinking your original remark referred to the module doc string.
Unfortunately this has now landed in master. Maybe the best thing to do is for me to include an update to this doc string as part of my next PR in a day or so.
There was a problem hiding this comment.
It's almost as if you intended this generalization from the beginning, given how easy the fixes were!
bors d+
(though feel free to wait for a review from @jcommelin)
|
✌️ ocfnash can now approve this pull request. To approve and merge a pull request, simply reply with |
leanprover-community-mathlib4-bot
added
delegated
and removed
awaiting-review
I had not intended it and I was surprised myself! bors merge |
|
Canceled. |
|
This seems to have been cancelled by a bot; I'm guessing this was because I sent it to bors while it was still building (bors was empty and I had just updated a doc string). I will thus try again. bors merge |
|
@ocfnash: I cancelled it, see #8546 (comment) |
|
Pull request successfully merged into master. Build succeeded: |
mathlib-bors
bot
changed the title
