Commit 2021-09-10 18:48 7500529f
View on Github →refactor(analysis/convex/basic): generalize segments to vector spaces (#9094)
segment
and open_segment
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.