New PR on ConicalHull and cone tensor products

Stream: new members

[Bjørn Solheim]

Hello everyone out there in the wonderful world of Lean and mathlib!

My name is Bjorn Solheim.

I just created a PR (https://github.com/leanprover-community/mathlib4/pull/27509)
pertaining to conical hulls and cone tensor products.
This is my first attempt at contributing.

The tensor product of two ordered vector spaces can be ordered in more than one way.
One way to deal with this is to define a range of possible tensor products for cones.
I hope this PR can perhaps contribute to formalizing such results.

Anyways, any comments are of course welcome.
Lots more for me to learn about formalizing mathematics.
And thanks to everyone for creating this amazing formalized mathematics platform and building
what seems to be an equally amazing community.