chore(analysis/convex/basic): instance cleanup (#9466)
Some lemmas were about `f : whatever → 𝕜`. They are now about `f : whatever → β` + a scalar instance between `𝕜` and `β`.
Some `add_comm_monoid` assumptions are actually promotable to `add_comm_group` directly thanks to [`module.add_comm_monoid_to_add_comm_group`](https://leanprover-community.github.io/mathlib_docs/algebra/module/basic.html#module.add_comm_monoid_to_add_comm_group). [Related Zulip discussion](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Convexity.20refactor/near/255268131).
