linear maps

Stream: new members

[Damiano Testa]

Dear All,

I am trying to use linear maps and I image that there is a better way to define mul_right in the code below. I suspect that I am missing something very simple.

In what follows, R is a comm_ring, M, N, P are R-modules.

Given a term f of Type M →ₗ[R] N →ₗ[R] P and an n : N, I want to define

def mul_right (n : N) : M →ₗ[R] P :=
{ to_fun := λ m, f m n,
  map_add' := λ x y, by simp only [linear_map.add_apply, linear_map.map_add],
  map_smul' := λ x y, by simp only [linear_map.smul_apply, linear_map.map_smul] }

This definition works, but I wonder if I really have to prove all the linearity stuff: I imagine that this is not the "correct" way of using bundled linear maps, but I do not know how to do it otherwise.

[Johan Commelin]

Isn't this f.flip n?

[Damiano Testa]

Yes it is! Thanks!