[Merged by Bors] - doc(algebra/algebra/basic): expand the docstring #10221
Conversation
eric-wieser
added
awaiting-review
jcommelin
added
awaiting-author
eric-wieser
added
awaiting-review
|
The new docstring is nice but it gets cut off in tool tips. So it should begin with a short explanation. |
|
I guess it makes sense to put this as the docstring to |
robertylewis
added
awaiting-author
eric-wieser
added
awaiting-review
|
I decided that this probably made more sense in an "implementation notes" section after all. |
| 1. ```lean | ||
| variables [comm_semiring R] [semiring A] | ||
| variables [algebra R A] | ||
| ``` | ||
| 2. ```lean | ||
| variables [comm_semiring R] [semiring A] | ||
| variables [module R A] [smul_comm_class R A A] [is_scalar_tower R A A] | ||
| ``` |
There was a problem hiding this comment.
I would state even more clearly: (1) is the preferred way of working with associative unital algebras. Something like
You should always use the first approach when working with associative unital algebras, but if you want to weaken any condition on either
RorAyou can mimic the second approach.
Other than that. LGTM.
bors d+
There was a problem hiding this comment.
I've added that at the end.
|
✌️ eric-wieser can now approve this pull request. To approve and merge a pull request, simply reply with |
fpvandoorn
added
delegated
|
bors merge |
github-actions
bot
added
the
ready-to-merge
This doesn't rule out having a better way to spell "non-unital non-associative algebra" in future, but let's document how it can be done today. Much of this description is taken from [my talk at CICM's FMM](https://eric-wieser.github.io/fmm-2021/#/algebras).
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
|
|
||
| example {R A} [comm_semiring R] [semiring A] | ||
| [module R A] [smul_comm_class R A A] [is_scalar_tower R A A] : algebra R A := | ||
| algebra.of_module smul_mul_assoc mul_smul_comm |
There was a problem hiding this comment.
I don't think I actually meant to commit this, but I guess it's harmless!
This doesn't rule out having a better way to spell "non-unital non-associative algebra" in future, but let's document how it can be done today.
Much of this description is taken from my talk at CICM's FMM.