Skip to content

Commit

Permalink
doc(Algebra/Group/Defs): add note on names SMul, VAdd; typo fix (#…
Browse files Browse the repository at this point in the history
…9776)

Edited module docstring:
* Fixed recent accidental damage
* Added a note about the motivation for the names `SMul` and `VAdd`
[Zulip discussion](https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/.60SMul.60.20and.20.60VAdd.60)


Co-authored-by: Richard Copley <rcopley@gmail.com>
  • Loading branch information
bustercopley and bustercopley committed Jan 23, 2024
1 parent e53e613 commit 029e239
Showing 1 changed file with 4 additions and 1 deletion.
5 changes: 4 additions & 1 deletion Mathlib/Algebra/Group/Defs.lean
Expand Up @@ -28,12 +28,15 @@ The file does not contain any lemmas except for
For basic lemmas about these classes see `Algebra.Group.Basic`.
We also introduce notation classes `lul` and `VAdd` for multiplicative and additive
We also introduce notation classes `SMul` and `VAdd` for multiplicative and additive
actions and register the following instances:
- `Pow M ℕ`, for monoids `M`, and `Pow G ℤ` for groups `G`;
- `SMul ℕ M` for additive monoids `M`, and `SMul ℤ G` for additive groups `G`.
`SMul` is typically, but not exclusively, used for scalar multiplication-like operators.
See the module `Algebra.AddTorsor` for a motivating example for the name `VAdd` (vector addition)`.
## Notation
- `+`, `-`, `*`, `/`, `^` : the usual arithmetic operations; the underlying functions are
Expand Down

0 comments on commit 029e239

Please sign in to comment.