gsmul and smul commute

Stream: Is there code for X?

[Eric Wieser]

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

[Eric Wieser]

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

[Eric Wieser]

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

[Eric Wieser]

#5135