Commit 2026-05-20 16:45 bb1f4068
View on Github →feat(Geometry/Convex): modules are convex spaces (#39531)
Show that every semimodule over an ordered semiring is a convex space.
It is sadly impossible to make this a global instance since it creates diamonds with structural instances such as ConvexSpace R X → ConvexSpace R Y → ConvexSpace R (X × Y) because (∑ i, f i).fst = ∑ i, (f i).fst isn't defeq, ultimately because Finset.sum isn't a field of AddCommMonoid.