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_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.

Estimated changes