mathlib

def1c02a - refactor(analysis/convex/function): generalize definition of `convex_on`/`concave_on` to allow any (ordered) scalars (#9389)

refactor(analysis/convex/function): generalize definition of `convex_on`/`concave_on` to allow any (ordered) scalars (#9389) `convex_on` and `concave_on` are currently only defined for real vector spaces. This generalizes ℝ to an arbitrary `ordered_semiring` in the definition.