[Merged by Bors] - feat: add Metric.Bounded.vadd

[urkud]

Add Metric.Bounded.smul and Metric.Bounded.vadd, rename the old smul to smul₀.

---

[ADedecker]

Could you add a comment on Metric.Bounded.smul along the lines of "This result is about isometric actions, see Metric.Bounded.smul₀ for the result for NormedSpaces". I could very well imagine searching for the NormedSpace lemma and searching for this exact name.

[urkud]

Could you add a comment on Metric.Bounded.smul along the lines of "This result is about isometric actions, see Metric.Bounded.smul₀ for the result for NormedSpaces". I could very well imagine searching for the NormedSpace lemma and searching for this exact name.

I added some comments. Feel free to edit them.

[ADedecker]

The docstrings are perfect, thanks.

maintainer merge

[github-actions]

🚀 Pull request has been placed on the maintainer queue by ADedecker.

[PatrickMassot]

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

• Build
• Check all files imported
• Lint style