Impmentation note uses Lean 3 instead of Lean 4

Stream: new members

[Omar Mohsen]

I found that in the implementation note of Normed algebra, the text you see when you hover over it in lean, uses the command

variables

instead of

variable

This probably appears elsewhere as well.

[Moritz Doll]

Good find! It would be great if you create a PR to fix that - should be an easy search to see whether that happened in other docstrings as well