## Stream: Is there code for X?

### Topic: gsmul and smul commute

#### 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


#### 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


#### 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?

#### Eric Wieser (Nov 27 2020 at 18:37):

#5135

Last updated: May 16 2021 at 05:21 UTC