Apurva
Lean is unable to automatically infer `ordered_smul` instance for `fin n → ℝ` from [docs#ordered_smul'](https://leanprover-community.github.io/mathlib_docs/algebra/order/module.html#pi.ordered_smul'). This in turns leads to issues with defining the [docs#convex_cone.positive](https://leanprover-community.github.io/mathlib_docs/find/convex_cone.positive) in these vector spaces. [Zulip...
Proof that the dual of dual of a closed convex cone is itself. I'll break this result into smaller PRs. This result is fundamental to formalising linear (or rather conic)...