Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-08-29 04:30 ea177c2a

View on Github →

feat(analysis/convex): add correspondence between convex cones and ordered semimodules (#3931) This shows that a convex cone defines an ordered semimodule and vice-versa.

Estimated changes