Bicommutant

Stream: Is there code for X?

[Aaron Anderson]

I'm not finding the following instance:

namespace module
namespace End

instance : module (module.End R M) M :=
{ smul := λ f, f,
  smul_zero := linear_map.map_zero,
  smul_add := linear_map.map_add,
  one_smul := λ x, rfl,
  zero_smul := λ x, rfl,
  mul_smul := λ x y b, rfl,
  add_smul := λ r s x, rfl, }

end End
end module

[Aaron Anderson]

Am I just missing this? If not, where should this belong?