Commit 2021-09-20 18:11 175afa8a
View on Github →refactor(analysis/convex/{extreme, exposed}): generalize is_extreme
and is_exposed
to semimodules (#9264)
is_extreme
and is_exposed
are currently only defined in real vector spaces. This generalizes ℝ to arbitrary ordered_semiring
s 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
.