[Merged by Bors] - feat(LocallyConvex/Bounded): add IsVonNBounded.add etc

[urkud]

• add IsVonNBounded.add, IsVonNBounded.vadd,
  and isVonNBounded_vadd;
• generalize some lemmas in Topology/Algebra/Monoid
  from Monoid to MulOneClass,
  move them to a new section.

---

[YaelDillies]

Suggested change

	theorem IsVonNBounded.right_of_add (hst : IsVonNBounded 𝕜 (s + t)) (hs : s.Nonempty) :
	theorem IsVonNBounded.of_add_right (hst : IsVonNBounded 𝕜 (s + t)) (hs : s.Nonempty) :

[urkud]

With of_add_right, it's not clear (for me) whether it's "of adding something on the right" (so this one should be of_add_left, see Int.ModEq.of_mul_left) or "of add, version for right term".

[YaelDillies]

That's fine, because both interpretations mean the same thing. We already used this pattern in other places.

[urkud]

Should this lemma be of_add_left or of_add_right?

[urkud]

I also used left_of_* in, e.g., left_ne_zero_of_mul. I don't care about this case (e.g., feel free to push a change to this PR) but we should choose one style some day. For now, for all lemmas ending with left/right, I try both every time.

[YaelDillies]

The difference between left_ne_zero_of_mul and here is that we have access to dot notation here, which means that we flush the left/right to the end of the lemma name.

[YaelDillies]

I renamed the lemmas so that they match Set.Nonempty.of_add_left/Set.Nonempty.of_add_right.

maintainer merge

[github-actions]

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

[sgouezel]

bors r+
Thanks!

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Check all files imported
• Lint style