stuck on generalising finsupp.to_module

Stream: maths

[Johan Commelin]

I really don't see why I'm getting stuck here. See the two comment lines just after the first sorry.

/- should this be stronger? [module γ β] → module γ (α →₀ β) -/   -- yes!
def to_module [decidable_eq γ] [ring β] [module β γ] : module β (α →₀ γ) :=
{ smul     := begin
                intros r f,
                apply f.map_range ((•) r) _,
                simp
              end, -- (•)
  smul_add := begin
                intros r f g,
                apply finsupp.ext,
                intro a,
                simp,
                rw smul_add,
                sorry
  end, -- assume a x y, finsupp.ext $ by simp [mul_add], -- original
  -- assume a x y, finsupp.ext $ by simp [map_range,smul_add], -- why doesn't this one work? <=====
  add_smul := sorry, --assume a x y, finsupp.ext $ by simp [add_mul],
  one_smul := assume x, finsupp.ext $ by simp,
  mul_smul := assume r s x, finsupp.ext $ by simp [mul_smul],
  .. finsupp.add_comm_group }

[Johan Commelin]

Never mind. I just realised that is_linear_map is not a class. Not going down the rabbit hole of modules.

[Kenny Lau]

linear_map is

[Johan Commelin]

And where does that beast live?

[Johan Commelin]

not in algebra/module

[Johan Commelin]

Ok, I found it... thanks!