Scalar multiplication on the right

Stream: Is there code for X?

[Anne Baanen]

We have docs#linear_map.lsmul. Isn't there a right multiplication version that doesn't need commutativity? It's not hard to show:

def linear_map.rsmul (R : Type*) {M : Type*} [semiring R] [add_comm_monoid M] [module R M] (y : M) : R →ₗ[R] M :=
{ to_fun := λ r, r • y,
  map_add' := λ r s, add_smul r s y,
  map_smul' := λ r s, smul_assoc r s y }

[Yury G. Kudryashov]

We have docs#linear_map.smul_right

[Anne Baanen]

That (linear_map.id.smul_right y) works, thanks!

[Yury G. Kudryashov]

Probably, we should have a name for this specific linear map.

[Yury G. Kudryashov]

It is used, e.g., in the definition of src#has_deriv_at_filter

[Eric Wieser]

docs#linear_map.to_span_singleton is that map

[Anne Baanen]

That's an unhelpful name...

[Eric Wieser]

Definitely

[Eric Wieser]

I also feel like smul_right ought to be defined in terms of it, not vice versa