doc: improve variable names and specify types in SMul doc

[AxelBoldt]

When documenting smul : M → α → α, it is unintuitive and confusing to use variables a:M and b:α. It is better to use m:M and a:α. I also specified the types of all involved terms in the documentation text.

[leanprover-community-bot]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 808d123e6f8b8eb40015aea3219d89d97c0c3abe --onto 3a42ee0c3060e2a8365927d205ead5990366053d. You can force Mathlib CI using the force-mathlib-ci label. (2025-10-27 17:44:57)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 808d123e6f8b8eb40015aea3219d89d97c0c3abe --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-10-27 17:44:58)

[TwoFX]

Thanks!