Zulip Chat Archive

Stream: Is there code for X?

Topic: Bicommutant


view this post on Zulip Aaron Anderson (Jan 10 2021 at 04:43):

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

view this post on Zulip Aaron Anderson (Jan 10 2021 at 04:45):

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


Last updated: May 16 2021 at 05:21 UTC