convex_on of linear_map

Stream: Is there code for X?

[Yaël Dillies]

We know that composition of a convex function by a linear map is convex as well, but it seems that we have nowhere that a linear map itself is convex. Am I right? It should be easy to fix.

[Anatole Dedecker]

I don't know if we have it, but I think the proof is just convex_on_id.comp_linear_map f

[Yaël Dillies]

I just went with three rw. Does the job! #7933