Commit 2021-09-16 13:26 89b0cfbf
View on Github →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.