mathlib3

89b0cfbf - refactor(analysis/convex/basic): generalize convexity to vector spaces (#9058)

refactor(analysis/convex/basic): generalize convexity to vector spaces (#9058) `convex` and `convex_hull` are currently only defined in real vector spaces. This generalizes ℝ to arbitrary ordered_semirings in definitions and abstracts it away to the correct generality in lemmas. It also generalizes the space from `add_comm_group` to `add_comm_monoid` where possible.