action on a constant is a linear_map

Stream: Is there code for X?

[Eric Wieser]

Do we have this definition somewhere?

def smul_lmap {R M : Type*} [semiring R] [add_comm_monoid M] [module R M] (m : M) : R →ₗ[R] M :=
{ to_fun := λ r, r • m,
  map_add' := λ r s, add_smul r s _,
  map_smul' := λ r x, smul_assoc _ _ _, }

docs#smul_const_hom (aka docs#distrib_mul_action.to_add_monoid_hom) and docs#smul_add_hom don't quite have as much structure as I want.

[Eric Wieser]

Wow, library_search found it, docs#linear_map.to_span_singleton

[Kevin Buzzard]

It's great when that works! The only caveat is that sometimes it finds eg the zero map :-)

[Eric Wieser]

That's what I expected it to find here

[Oliver Nash]

Sometimes suggest helps in these cases.