representations of k-algebras

Stream: Is there code for X?

[Scott Morrison]

Where might I find:

def foo {k A V : Type*} [comm_ring k] [ring A] [algebra k A] [add_comm_group V]
  [module k V] [module A V] [smul_comm_class k A V] :
  A →ₐ[k] (V →ₗ[k] V) :=
sorry

[Eric Wieser]

I don't think I ever added that one

[Eric Wieser]

It would be called docs#algebra.to_module_End

[Eric Wieser]

But I didn't go any further than docs#module.to_module_End

[Scott Morrison]

Oh, I think it actually needs is_scalar_tower, not just smul_comm_class, for the commutes' field. I'll go install it.

[Eric Wieser]

(don't forget to relax ring to semiring)

[Eric Wieser]

Ah, this does exist after all; it's docs#algebra.lsmul

[Eric Wieser]

Perhaps we should rename it for consistency

[Scott Morrison]

Ok, I've reverted to using lsmul.