doc: add reassoc docstring

[kbuzzard]

trafficstars

Add docstring for @[reassoc] attribute.

---

Note that, in contrast to when I'm adding maths docstrings, here I know far less about what I'm talking about (in particular I can't read the source code to verify that what I'm saying corresponds to what is written). I'm making this PR because of a general frustration about attributes not being documented properly. This PR makes the docstring added here appear when hovering over @[reassoc]. My sources are the module docstring for the attribute, and the comment here by Markus Himmel. I also fix a couple of typos in the module docstring.

[github-actions[bot]]

PR summary 0364e4957c

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

No declarations were harmed in the making of this PR! 🐙

You can run this locally as follows

## summary with just the declaration names:
./scripts/no_lost_declarations.sh short <optional_commit>

## more verbose report:
./scripts/no_lost_declarations.sh <optional_commit>

[joelriou]

It looks good to me. If you would like, you may also mention that the combination @[simp, reassoc] is possible. This can be useful for lemmas of the form f = a ≫ b, i.e. no composition in the LHS, but we may occasionally want to apply the _assoc version in the other direction: replacing a ≫ b ≫ h by f ≫ h.

[joelriou]

Thanks!

bors d+

[mathlib-bors[bot]]

:v: kbuzzard can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[kbuzzard]

bors r+

[mathlib-bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style