linear map from bilinear

Stream: Is there code for X?

[Rémy Degenne]

We have docs#continuous_linear_map.lsmul which is a continuous bilinear map 𝕜' →L[𝕜] E →L[𝕜] E for the scalar multiplication λ r x, r • x. I want to use the linear map 𝕜' →L[𝕜] E corresponding to λ r, r • x for a fixed x.
Is there a definition somewhere that gives the linear map obtained by fixing the second argument in a bilinear map? Something of the form (E →L[𝕜] F →L[𝕜] G) → (E →L[𝕜] G).

A way to get the linear map I want is to use docs#continuous_linear_map.flip to reverse the arguments of 𝕜' →L[𝕜] E →L[𝕜] E and get E →L[𝕜] 𝕜' →L[𝕜] E and then just apply it to x : E. Is there a name for this in mathlib?

[Johan Commelin]

I think mostly .flip is what is used, like you said. I'm not aware of other defs/methods.

[Rémy Degenne]

Thanks. I'll use flip then.

[Eric Wieser]

I think that's docs#linear_map.to_span_singleton?

[Eric Wieser]

For which there is probably no continuous version yet.

[Rémy Degenne]

Thanks! It's indeed not continuous, but it's good to know that something like that exists. I would never have guessed the nameto_span_singleton.

[Eric Wieser]

I found it via library_search when looking for the non-continuous version. I agree the name is strange.

[Eric Wieser]

There's also docs#continuous_linear_equiv.to_span_nonzero_singleton from #3021 that introduces both defs