Zulip Chat Archive

Stream: Is there code for X?

Topic: gsmul and smul commute


view this post on Zulip Eric Wieser (Nov 27 2020 at 18:11):

example {R : Type*} {L : Type*} {ι : Type*}
  [semiring R] [add_comm_group L] [semimodule R L]
  (y : ) (c : R) (x : L) :
  y  c  x = c  (y  x) :=
begin
  rw [gsmul_eq_smul, gsmul_eq_smul],  -- does this help? Which is more canonical?
  sorry
end

view this post on Zulip Eric Wieser (Nov 27 2020 at 18:25):

instance nsmul.smul_comm [semiring R] [add_comm_monoid M] [semimodule R M] : smul_comm_class  R M :=
{ smul_comm := λ n r m, begin
    dsimp [()],
    induction n with n ih,
    { simp },
    { simp [succ_nsmul, ih] },
  end }

instance gsmul.smul_comm [semiring R] [add_comm_group L] [semimodule R L] : smul_comm_class  R L :=
{ smul_comm := λ z r l, by cases z; simp [gsmul_eq_smul, nat.smul_def, smul_comm] }

example {R : Type*} {L : Type*} {ι : Type*}
  [semiring R] [add_comm_group L] [semimodule R L]
  (y : ) (c : R) (x : L) :
  y  c  x = c  (y  x) :=
begin
  rw [gsmul_eq_smul, gsmul_eq_smul],
  apply smul_comm y c x,
end

view this post on Zulip Eric Wieser (Nov 27 2020 at 18:27):

@Yury G. Kudryashov, since you wrote smul_comm_class, do you have an opinion on where I should put those instances?

view this post on Zulip Eric Wieser (Nov 27 2020 at 18:37):

#5135


Last updated: May 16 2021 at 05:21 UTC