Def convex_cone.to_ordered_semimodule

Modification history

2020-10-30 08:20
src/analysis/convex/cone.lean
refactor(module/ordered): make ordered_semimodule a mixin (#4719) …
Deleted convex_cone.to_ordered_semimoduleView on Github →
2020-08-29 04:30
src/analysis/convex/cone.lean
feat(analysis/convex): add correspondence between convex cones and ordered semimodules (#3931) …
Added convex_cone.to_ordered_semimoduleView on Github →