apply linear_map

Stream: Is there code for X?

[Patrick Massot]

Am I missing

def linear_map.applyₗ (v : M) : (M →ₗ[R] M₂) →ₗ[R] M₂ :=
{ to_fun := λ f, f v,
  map_add' := λ f g, f.add_apply g v,
  map_smul' := λ x f, f.smul_apply x v }