## Stream: Is there code for X?

### Topic: finsupp gsmul_eq_smul

#### Kevin Buzzard (Aug 25 2020 at 13:57):

example (n : ) (α : Type) (x : α  ) : n  x = n  x :=
begin
rw gsmul_eq_smul,
-- ⊢ n • x = n • x
congr',
-- ⊢ finsupp.has_scalar = mul_action.to_has_scalar
sorry
end

I'm stuck

does ext help?

yes

module  (α  )

#### Kevin Buzzard (Aug 25 2020 at 14:08):

example (n : ) (α : Type) (x : α  ) : n  x = n  x :=
begin
rw module.gsmul_eq_smul_cast ,
simp,
apply_instance
end

#### Kevin Buzzard (Aug 25 2020 at 14:09):

example (n : ) (α : Type) (x : α  ) : n  x = n  x :=
by rw [module.gsmul_eq_smul_cast  n x, int.cast_id n]

Thanks

#### Kevin Buzzard (Aug 25 2020 at 17:44):

/-- The natural ℤ-module structure on any add_comm_group. -/
-- We don't immediately make this a global instance, as it results in too many instances,
-- and confusing ambiguity in the notation n • x when n : ℤ.
-- We do turn it into a global instance, but only at the end of this file,
-- and I remain dubious whether this is a good idea.
def int_module : module  M :=

(Scott said this in algebra.module.basic). This is exactly what I've been seeing with finsupp.

I think these are missing:

lemma finsupp.smul_eq_nsmul {α : Type u} {B : Type v} [add_comm_monoid B] (n : )
(x : α  B) : n  x = n  x :=
ext $λ a, nat.rec_on n rfl$ λ d hd,