Stream: new members

Topic: linear maps

Damiano Testa (Feb 25 2021 at 07:45):

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_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 (Feb 25 2021 at 07:53):

Isn't this f.flip n?

Damiano Testa (Feb 25 2021 at 07:55):

Yes it is! Thanks!

Last updated: May 12 2021 at 23:13 UTC